STRIP: Structural Sharing for Efficient Proof-search

Dominique Larchey-Wendling (1) , Daniel Mery (1) , Didier Galmiche (1)

1 TYPES - Logic, proof Theory and Programming

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.

Domaines: Algorithme et structure de données [cs.DS]; Intelligence artificielle [cs.AI]; Logique en informatique [cs.LO]

Dominique Larchey-Wendling, Daniel Mery, Didier Galmiche. STRIP: Structural Sharing for Efficient Proof-search. 2001, Siena, Italy, pp.696 - 700. ⟨hal-00008805⟩