Source: leo2 Section: misc Priority: extra Maintainer: Jonathan von Schroeder Build-Depends: debhelper (>= 7.4.15), zlib1g-dev, help2man, ocaml, ocaml-findlib, camlp4 Standards-Version: 3.9.2 Homepage: http://page.mi.fu-berlin.de/cbenzmueller/leo/index.html 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.