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
There are currently no files to download. Check again soon.Related Downloads
The following classes are related to this project and were held at Freie Universität Berlin:
Links to similar or related projects: