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.
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.