Overview
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. LEO-II was the first theorem prover to support THF, FOF and CNF syntax.
LEO-II is implemented in Objective CAML and its problem representation language is TPTP THF.
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.