LEO-II
LEO-II is a standalone, resolution-based higher-order theorem prover designed for fruitful cooperation with specialist provers for natural fragments of higher-order logic. At present LEO-II can cooperate with TPTP compliant first-order automated theorem provers such as E, SPASS, Gandalf and Vampire. World Champion 2010: LEO-II was the winner of the THF division (automation of higher-order logic) at CASC-J5. At CASC-J23 in 2011 LEO-II finished second in the THF division. Moreover, at CASC-J5 and CASC-23 LEO-II did also participate in the first-order divisions FOF and CNF and performed reasonably well. LEO-II has been the first theorem prover that supports THF, FOF and CNF syntax. LEO-II is implemented in Objective CAML and its problem representation language is TPTP THF.
Keywords for this software
References in zbMATH (referenced in 51 articles , 1 standard article )
Showing results 1 to 20 of 51.
Sorted by year (- Benzmüller, Christoph; Scott, Dana S.: Automating free logic in HOL, with an experimental application in category theory (2020)
- Kaufmann, Matt; Moore, J. Strother: Limited second-order functionality in a first-order setting (2020)
- Barbosa, Haniel; Reynolds, Andrew; El Ouraoui, Daniel; Tinelli, Cesare; Barrett, Clark: Extending SMT solvers to higher-order logic (2019)
- Brown, Chad E.; Gauthier, Thibault; Kaliszyk, Cezary; Sutcliffe, Geoff; Urban, Josef: GRUNGE: a grand unified ATP challenge (2019)
- Bentkamp, Alexander; Blanchette, Jasmin Christian; Cruanes, Simon; Waldmann, Uwe: Superposition for (\lambda)-free higher-order logic (2018)
- Benzmüller, Christoph; Parent, Xavier; van der Torre, Leendert: A deontic logic reasoning infrastructure (2018)
- Lopez Hernandez, Julio Cesar; Korovin, Konstantin: An abstraction-refinement framework for reasoning with large theories (2018)
- Lvov, M.; Peschanenko, V.; Letychevskyi, O.; Tarasich, Y.; Baiev, A.: Algorithm and tools for constructing canonical forms of linear semi-algebraic formulas (2018)
- Benzmüller, Christoph: Cut-elimination for quantified conditional logic (2017)
- Benzmüller, C.; Weber, Leon; Woltzenlogel Paleo, Bruno: Computer-assisted analysis of the Anderson-Hájek ontological controversy (2017)
- Gleißner, Tobias; Steen, Alexander; Benzmüller, Christoph: Theorem provers for every normal modal logic (2017)
- Schulz, Stephan; Sutcliffe, Geoff; Urban, Josef; Pease, Adam: Detecting inconsistencies in large first-order knowledge bases (2017)
- Benzmüller, Christoph; Woltzenlogel Paleo, Bruno: An object-logic explanation for the inconsistency in Gödel’s ontological theory (2016)
- Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
- Brown, Chad E.; Urban, Josef: Extracting higher-order goals from the Mizar Mathematical Library (2016)
- Wisniewski, Max; Steen, Alexander; Kern, Kim; Benzmüller, Christoph: Effective normalization techniques for HOL (2016)
- Benzmüller, Christoph: Higher-order automated theorem provers (2015)
- Benzmüller, Christoph: Invited talk: on a (quite) universal theorem proving approach and its application in metaphysics (2015)
- Benzmüller, Christoph; Paleo, Bruno Woltzenlogel: On logic embeddings and Gödel’s god (2015)
- Benzmüller, Christoph; Paleo, Bruno Woltzenlogel: Interacting with modal logics in the coq proof assistant (2015)
Further publications can be found at: http://page.mi.fu-berlin.de/cbenzmueller/leo/references.html