Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic. In this paper we describe Imogen, a theorem prover for intuitionistic propositional logic using the focused inverse method. We represent fine-grained control of the search behavior by polarizing the input formula. In manipulating the polarity of atoms and subformulas, we can often improve the search time by several orders of magnitude. We tested our method against seven other systems on the propositional fragment of the ILTP library. We found that our prover outperforms all other provers on a substantial subset of the library.
References in zbMATH (referenced in 7 articles )
Showing results 1 to 7 of 7.
- Ferrari, Mauro; Fiorentini, Camillo; Fiorino, Guido: JTabWb: a Java framework for implementing terminating sequent and tableau calculi (2017)
- Chaudhuri, Kaustuv; Marin, Sonia; Straßburger, Lutz: Focused and synthetic nested sequents (2016)
- Brock-Nannestad, Taus; Chaudhuri, Kaustuv: Disproving using the inverse method by iterative refinement of finite approximations (2015)
- Ferrari, Mauro; Fiorentini, Camillo; Fiorino, Guido: fCube: an efficient prover for intuitionistic propositional logic (2010)
- McLaughlin, Sean; Pfenning, Frank: Efficient intuitionistic theorem proving with the polarized inverse method (2009)
- Cervesato, Iliano (ed.); Veith, Helmut (ed.); Voronkov, Andrei (ed.): Logic for programming, artificial intelligence, and reasoning. 15th international conference, LPAR 2008, Doha, Qatar, November 22--27, 2008. Proceedings (2008)
- McLaughlin, Sean; Pfenning, Frank: Imogen: Focusing the polarized inverse method for intuitionistic propositional logic (2008)