-
Notifications
You must be signed in to change notification settings - Fork 1
System LEO II
Christoph Benzmüller, Frank Theiss and Nik Sultana.
LEO-II is a standalone, resolution-based theorem prover for higher-order logic (HOL) 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.
It is is implemented in Objective CAML and open-source under BSD 3-Clause License.
- Proving
- Model finding
The input language is TPTP THF, more precisely its monomorphic variant TH0. This corresponds to simply typed classical higher-order logic, including, e.g., quantification over functions and predicates. Additionally, LEO-II also supports reasoning with choice.
LEO-II can output proofs in the TSTP format.
LEO-II was the winner of the THF division (automation of higher-order logic) at CASC-J5. LEO-II was the first theorem prover to support THF, FOF and CNF syntax.
The development of LEO-II was supported by the EPRSC grant EP/D070511/1 at Cambridge University, England. Subsequently the project received support from EU grant PIIF-GA-2008-219982 (THFTPTP) and the German BMBF project Verisoft XT. More recently, LEO-II has been supported by the DFG research grant BE 2501/6-1 ONTOLEO.
LEO-II is included in the Sledgehammer tool of Isabelle/HOL.
Archived at https://github.com/leoprover/LEO-II
The Higher-Order Prover LEO-II. Benzmüller, C., Sultana, N., Paulson, L. C., & Theiss, F. Journal of Automated Reasoning, 55(4): 389-404, 2015. DOI: 10.1007/978-3-319-94205-6_8. Preprint available at https://tinyurl.com/y7wg5w5w.