Imogen swMATH ID: 11384 Software Authors: Sean McLaughlin; Frank Pfenning Description: 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. Homepage: http://link.springer.com/chapter/10.1007/978-3-540-89439-1_12 Related Software: ILTP; fCube; IntHistGC; ileanCoP; LoTREC; STRIP; JTabWb; Twelf; Easychair; TABLEAUX; Coq; intuit; Isabelle; Cool; MetTeL; CoLoSS; PVS; Mace4; MiniSat; BDDIntKt Cited in: 11 Publications all top 5 Cited by 16 Authors 3 Ferrari, Mauro 3 Fiorentini, Camillo 2 Chaudhuri, Kaustuv 2 Fiorino, Guido 2 McLaughlin, Sean 2 Pfenning, Frank 1 Brock-Nannestad, Taus 1 Burel, Guillaume 1 Cervesato, Iliano 1 Dyckhoff, Roy 1 Goré, Rajeev Prabhakar 1 Marin, Sonia 1 Straßburger, Lutz 1 Thomson, Jimmy 1 Veith, Helmut 1 Voronkov, Andrei Cited in 3 Serials 1 Journal of Automated Reasoning 1 Fundamenta Informaticae 1 Lecture Notes in Computer Science Cited in 3 Fields 10 Mathematical logic and foundations (03-XX) 9 Computer science (68-XX) 1 General and overarching topics; collections (00-XX) Citations by Year