The Leo-III Project

ABSTRACT. We report on the recently started Leo-III project, in which we design and implement a state-of-the-art Higher-Order Logic Theorem Prover, the successor of the well known LEO-II prover. Leo-III will be 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 archi- tecture 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.