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.

References in zbMATH (referenced in 28 articles , 1 standard article )

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

1 2 next

  1. Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
  2. Brown, Chad E.; Urban, Josef: Extracting higher-order goals from the Mizar Mathematical Library (2016)
  3. Benzmüller, Christoph; Sultana, Nik; Paulson, Lawrence C.; Theiß, Frank: The higher-order prover Leo-II (2015)
  4. Foster, Simon; Struth, Georg: On the fine-structure of regular algebra (2015)
  5. Kühlwein, Daniel; Urban, Josef: MaLeS: a framework for automatic tuning of automated theorem provers (2015)
  6. Wisniewski, Max; Steen, Alexander; Benzmüller, Christoph: LeoPARD -- a generic platform for the implementation of higher-order reasoners (2015)
  7. Kaliszyk, Cezary; Urban, Josef: Learning-assisted automated reasoning with $\mathsfFlyspeck$ (2014)
  8. Benzmüller, Christoph; Paulson, Lawrence C.: Quantified multimodal logics in simple type theory (2013)
  9. Brown, Chad E.: Reducing higher-order theorem proving to a sequence of SAT problems (2013)
  10. Sultana, Nik; Blanchette, Jasmin Christian; Paulson, Lawrence C.: LEO-II and Satallax on the Sledgehammer test bench (2013)
  11. Brown, Chad E.: Satallax: an automatic higher-order prover (2012)
  12. Raths, Thomas; Otten, Jens: The QMLTP problem library for first-order modal logics (2012)
  13. Benzmüller, Christoph: Combining and automating classical and non-classical logics in classical higher-order logics (2011)
  14. Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.: Extending Sledgehammer with SMT solvers (2011)
  15. Brown, Chad E.: Reducing higher-order theorem proving to a sequence of SAT problems (2011)
  16. Rabe, Florian; Kohlhase, Michael; Sacerdoti Coen, Claudio: A foundational view on integration problems (2011)
  17. Backes, Julian; Brown, Chad E.: Analytic tableaux for higher-order logic with choice (2010)
  18. Benzmüller, Christoph: Combining logics in simple type theory (2010)
  19. Benzmüller, Christoph: Verifying the modal logic cube is an easy task (for higher-order automated reasoners) (2010)
  20. Benzmüller, Christoph; Paulson, Lawrence C.: Multimodal and intuitionistic logics in simple type theory (2010)

1 2 next