Effective Higher-Order Automated Theorem Proving

点击翻译按钮获取中文摘要

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.