STRIP: Structural Sharing for Efficient Proof-Search

The STRIP system is a theorem prover for intuitionistic propositional logic with two main characteristics: it deals with the duplication of formulae during proof-search from a fine and explicit management of formulae (as resources) based on a structural sharing and it builds, for a given formula, either a proof or a countermodel.

• Type: Conference
• Year: 2001
• Where: CADE
• Authors: Didier Galmiche, Dominique Larchey-Wendling, Dominique Méry
• Keywords: Automated Reasoning, CADE 2001, Intuitionistic Propositional Logic, Theorem Prover