Effective Higher-Order Automated Theorem Proving

• Applicant: Professor Dr.-Ing. Christoph Benzmüller
• Subject Area: Theoretical Computer Science ; Image and Language Processing, Computer Graphics and Visualisation, Human Computer Interaction, Ubiquitous and Wearable Computing
• Term: from 2014 to 2018
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 241609402

The automated theorem proving systems LEO-I and LEO-II have found international acclaim as very successful reasoners for classical higher-order logic. Novel contributions of LEO-I include a native (versus axiomatic) treatment of the extensionality principles and the cooperation with external reasoners (such as the first-order prover E) via a flexible agent architecture. The implementation of LEO-II did significantly influence the parallel development of the new higher-order TPTP THF infrastructure for typed higher-order logics, which in turn has led to major system improvements (e.g. in the automated theorem provers ISABELLE/HOL and TPS) and to new systems developments (such as Satallax) for classical higher-order logic. LEO-II has won the international CASC competition in 2010 and it is currently being integrated in the interactive proof assistant ISABELLE/HOL.In this project, we want to turn LEO-II into a theorem prover based on ordered paramodulation/ superposition.These modifications to LEO-II are significant both in theory and practice. The resulting system, called LEO-III, will put an emphasis on ease of integration with other systems.

• DFG Programme: Research Grants