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 competitions in 2010 and it has been integrated in the interactive proof assistant ISABELLE /HOL.
In this project, we want to turn LEO-II into a state-of-the-art theorem prover based on ordered paramodulation/ superposition. In constrast to LEO-II, we replace the internal term representation (the commonly used simply typed lambda calculus) by a more expressive system supporting type polymorphism. In the course of the project, we plan to further enhance the type system with type classes and type constructors similar to System Fω . In order to achieve a substantial performance speed-up, the architecture of Leo-III will be based on massive parallelism (e.g. And/Or-Parallelism, Multisearch).
The current design is a multi-agent blackboard architecture that will allow to independently run agents with our proof calculus as well as agents for external (specialized) provers. Leo-III will focus right from the start on compatibility to the widely used TPTP infrastructure. Moreover, it will offer built-in support for specialized external prover agents and provide external interfaces to interactive provers such as Isabelle/HOL. The implementation will excessively use term sharing and several indexing techniques. Leo-III will also offer special support for reasoning in various quantified non-classical logics by exploiting a semantic embedding approach.
The Leo-III project is supported by the German National Research Foundation (DFG) under grant BE 2501/11-1 (LEO-III).
Leo III is currently being developed by
with contributions from
Leo-III Version 1.1 is available!
The following classes are related to this project and were held at Freie Universität Berlin:
Links to similar or related projects: