Source: leo2
Section: misc
Priority: extra
Maintainer: Jonathan von Schroeder <jonathan.von_schroeder@dfki.de>
Build-Depends: debhelper (>= 7.4.15), zlib1g-dev, help2man, ocaml, ocaml-findlib, camlp4
Standards-Version: 3.9.2
Package: leo2
Architecture: any
Depends: ${shlibs:Depends}, ${misc:Depends}, eprover
Description: Higher-order theorem prover
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.
.
LEO-II was the winner of the THF division (automation of higher-order logic) at CASC-J5. At CASC-23 in 2011, LEO-II finished second in the THF category. LEO-II does also participate in the first-order divisions FOF and CNF. At present LEO-II is the only theorem prover available that supports THF, FOF and CNF syntax.
.
LEO-II is implemented in Objective CAML and its problem representation language is TPTP THF.