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