STRIP

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.


References in zbMATH (referenced in 14 articles , 2 standard articles )

Showing results 1 to 14 of 14.
Sorted by year (citations)

  1. Ferrari, Mauro; Fiorentini, Camillo; Fiorino, Guido: Contraction-free linear depth sequent calculi for intuitionistic propositional logic with the subformula property and minimal depth counter-models (2013)
  2. Galmiche, Didier; Larchey-Wendling, Dominique; Vidal-Rosset, Joseph: Some remarks on relations between proofs and games (2010)
  3. Ferrari, Mauro; Fiorentini, Camillo; Fiorino, Guido: A tableau calculus for propositional intuitionistic logic with a refined treatment of nested implications (2009)
  4. McLaughlin, Sean; Pfenning, Frank: Imogen: Focusing the polarized inverse method for intuitionistic propositional logic (2008)
  5. Raths, Thomas; Otten, Jens; Kreitz, Christoph: The ILTP problem library for intuitionistic logic (2007)
  6. Raths, Thomas; Otten, Jens; Kreitz, Christoph: The ILTP library: Benchmarking automated theorem provers for intuitionistic logic (2005)
  7. Galmiche, Didier; Méry, Daniel: Semantic labelled tableaux for propositional $\textBI^\perp$ (2003)
  8. Egly, Uwe: Embedding lax logic into intuitionistic logic (2002)
  9. Larchey-Wendling, Dominique: Combining proof-search and counter-model construction for deciding Gödel-Dummett logic (2002)
  10. Galmiche, Didier; Méry, Daniel: Proof-search and countermodel generation in propositional BI logic (2001)
  11. Larchey-Wendling, D.; Méry, D.; Galmiche, Didier: STRIP: Structural sharing for efficient proof-search (2001)
  12. Hirokawa, Sachio; Nagano, Daisuke: Long normal form proof search and counter-model generation. (2000)
  13. Hirokawa, Sachio; Nagano, Daisuke: Long normal form proof search and counter-model generation (2000)
  14. Galmiche, Didier; Larchey-Wendling, Dominique: Structural sharing and efficient proof-search in propositional intuitionistic logic (1999)