∀P.Leo III

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

• Christoph Benzmüller (Principal Investigator),
• Max Wisniewski,
• Alexander Steen,

with contributions from

• Tomer Libal,
• Maximilian Claus (Thesis),
• Kim Kern (Thesis),
• Hans-Jörg Schurr (Thesis),
• Samuel Gfrörer (Thesis),
• Irina Makarenko (Thesis) and
• Tobias Gleißner (Thesis),

Further collaborators:

• Frank Theiss
• Leon Weber
• Daniel Jentsch

Leo-III Version 1.3 is available!

• Executable Jar (~ 9MB)
• Source archive (~ 3MB)

See here for information about installation and usage of Leo-III. See also the GitHub release.

Older version: Leo-III 1.2, Leo-III 1.1, Leo-III 1.0

• Capability descriptions of the ATP systems
  • Leo-III: Download
  • LEO-II: Download
• ANTLR grammar file for TPTP languages (CNF, FOF, TFF, THF): tptp.g4
• LEOPARD (Leo-III's Parallel ARchitecture and Datastructures) is a generic system platform for implementing knowledge representation and reasoning tools (such as automated theorem prover) based on classical higher-order logic.
  The first relase of LeoPARD can be found at its GitHub repository.
• Modal Embedding Tool (MET): Pre-processor for higher-order quantified modal logic problems to plain TPTP TH0, see our GitHub project.

1. Alexander Steen, Extensional Paramodulation for Higher-Order Logic and its Effective Implementation Leo-III. Dissertation, Freie Universität Berlin. Published in Dissertations in Artificial Intelligence (DISKI), volume 345, EAN/ISBN 978-3-89838-739-2, AKA-Verlag, 2018.
2. Alexander Steen, Christoph Benzmüller, System Demonstration: The Higher-Order Prover Leo-III. In Christoph Benzmüller, Jens Otten (Eds.), ARQNL 2018. Automated Reasoning in Quantified Non-Classical Logics, Proceedings, CEUR Workshop Proceedings, http://ceur-ws.org, volume 2095, 2018.
3. Alexander Steen, Christoph Benzmüller, The Higher-Order Prover Leo-III. In Didier Galmiche, Stephan Schulz, Roberto Sebastiani (Eds.), Automated Reasoning --- 9th International Joint Conference, IJCAR 2018, Oxford, UK, July 14-17, 2018, Proceedings , Springer, LNCS, Volume 10900, pp. 108-116, 2018.
4. Christoph Benzmüller, Alexander Steen, Max Wisniewski Leo-III Version 1.1 (System description), In Thomas Eiter, David Sands, Geoff Sutcliffe and Andrei Voronkov (Eds.), IWIL Workshop and LPAR Short Presentations, EasyChair, Kalpa Publications in Computing, Volume 1, pp. 11-26, 2017.
5. Alexander Steen, Max Wisniewski, Christoph Benzmüller Going Polymorphic - TH1 Reasoning for Leo-III, In Thomas Eiter, David Sands, Geoff Sutcliffe and Andrei Voronkov (Eds.), IWIL Workshop and LPAR Short Presentations, EasyChair, Kalpa Publications in Computing, Volume 1, pp. 100-112, 2017.
6. Alexander Steen, Max Wisniewski, Christoph Benzmüller, Agent-Based HOL Reasoning. In 5th International Congress on Mathematical Software, ICMS 2016, Berlin, Germany, July 2016, Proceedings, Springer, LNCS, volume 9725. 2016.
7. Max Wisniewski, Alexander Steen, Kim Kern, Christoph Benzmüller, Effective Normalization Techniques for HOL. In Nicola Olivetti, Ashish Tiwari (Eds.), 8th International Joint Conference on Automated Reasoning, IJCAR 2016, Coimbra, Portugal, 27 June - 2 July, 2016, Proceedings. Springer, LNAI, 2016. 2016.
8. Max Wisniewski, Christoph Benzmüller, Is it Reasonable to Employ Agents in Theorem Proving?. In Jan van den Heerik, Joaquim Filipe (Eds.), Proceedings of the 8th International Conference on Agents and Artificial Intelligence (ICAART 2016) -- Volume 1, SCITEPRESS -- Science and Technology Publications, Lda, volume 1, pp. 281-286, 2016.
9. Max Wisniewski, Alexader Steen, Christoph Benzmüller, LeoPARD - A Generic Platform for the Implementation of Higher-Order Reasoners. In Conference on Intelligent Computer Mathematics (CICM 2015), 2015.
10. Max Wisniewski, Agent-based Blackboard Architecture for a Higher-Order Theorem Prover. Master Thesis, Freie Universität Berlin, revised version, 2014.
11. Alexander Steen, Efficient Data Structures for Automated Theorem Proving in Expressive Higher-Order Logics. Master Thesis, Freie Universität Berlin, revised version, 2014.
12. Max Wisniewski, Alexander Steen, Christoph Benzmüller, The Leo-III Project. In Alexander Bolotov, Manfred Kerber (eds.), Joint Automated Reasoning Workshop and Deduktionstreffen, 2014.
13. Christoph Benzmüller, Higher-Order Automated Theorem Provers. In David Delahaye and Bruno Woltzenlogel Paleo (eds.), All about Proofs, Proof for All, pp. 171-214. College Publications, 2014.

• Tobias Gleißner, Alexander Steen, The MET: The Art of Flexible Reasoning with Modalities. In Christoph Benzmüller, Francesco Ricca (Eds.), 2nd International Joint Conference on Rules and Reasoning (RuleML+RR 2018), Proceedings, Springer, LNCS, 2018.
• Tobias Gleißner, Alexander Steen, Christoph Benzmüller, Theorem Provers for Every Normal Modal Logic, In Thomas Eiter, David Sands (Eds.), LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, EasyChair, EPiC Series in Computing, Volume 46, pp. 14-30, 2017.
• Alexander Steen, Max Wisniewski, Hans-Jörg Schurr, Christoph Benzmüller Capability Discovery for Automated Reasoning Systems, In Thomas Eiter, David Sands, Geoff Sutcliffe and Andrei Voronkov (Eds.), IWIL Workshop and LPAR Short Presentations, EasyChair, Kalpa Publications in Computing, Volume 1, pp. 113-118, 2017.
• Alexander Steen, Max Wisniewski, Christoph Benzmüller, Einsatz von Theorembeweisern in der Lehre. In Andreas Schwill, Ulrike Lucke (Eds.), Hochschuldidaktik der Informatik, HDI2016 – 7. Fachtagung des GI-Fachbereichs Informatik und Ausbildung / Didaktik der Informatik ; 13.-14. September 2016 an der Universität Potsdam, Commentarii Informaticae Didacticae, Volume 10, pages 81 - 92, Universitätsverlag Potsdam, 2016.
• Alexander Steen, Christoph Benzmüller, Sweet SIXTEEN: Automation via Embedding into Classical Higher-Order Logic. In Logic and Logical Philosophy, Volume 25, No 4, Nicolaus Copernicus University, 2016.
• Alexander Steen, Max Wisniewski, Christoph Benzmüller, Tutorial on Reasoning in Expressive Non-Classical Logics with Isabelle/HOL. In Christoph Benzüller, Raul Rojas, Geoff Sutcliffe (Eds.), Second Global Conference on Artificial Intelligence (GCAI), Proceeedings, EasyChair, EPiC Series in Computing, Volume 41, pp. 1-10, 2016.
• Alexander Steen, Max Wisniewski, Christoph Benzmüller, Einsatz von Theorembeweisern in der Lehre. In 7. Fachtagung für Hochschuldidaktik der Informatik, Commentarii Informaticae Didacticae, Universitätsverlag Potsdam, 2016.
• Max Wisniewski, Alexander Steen, Christoph Benzmüller, TPTP and Beyond: Representation of Quantified Non-Classical Logics. In C. Benzmüller, J. Otten (Eds.), 2nd International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARNQL 2016), Coimbra, Portugal, July 2016, Proceedings, CEUR Workshop Proceedings, Volume 1770, CEUR-WS.org, 2016.
• Alexander Steen and Max Wisniewski, Embedding of First-Order Nominal Logic into HOL. 5th World Congress and School on Universal Logic, Istanbul, 2015.
• Christoph BenzmÜller and Bruno Woltzenlogel Paleo, On Logic Embeddings and Gödel’s God. In Proceedings of the 22nd International Workshop on Algebraic Development Techniques (WADT 2014), Sinaia, Romania, 2014.
• Christoph Benzmüller and Bruno Woltzenlogel Paleo, Automating Gödel's Ontological Proof of God's Existence with Higher-order Automated Theorem Prover. In Thorsten Schaub (ed.), 21st European Conference on Artificial Intelligence (ECAI), 2014.
• Yves Müller, Subprover Parallelism in the Automated Theorem Prover LEO-II. Master Thesis, Freie Universität Berlin, 2013.

Beniamino Accattoli (August 2017)

INRIA, PARSIFAL

Hans-Jörg Schurr (October 2015 - June 2017)

TU Wien

Max Haslbeck (Januar - October 2016)

TU München

Geoff Sutcliffe (September/October 2016)

University of Miami, Department of Computer Science

Jasmin Blanchette (April/May 2016)

INRIA Nancy and MPII Saarbrücken

Gerald Penn (April 2016)

Department of Computer Science, University of Toronto

Eric Cortlett (April 2016)

Department of Computer Science, University of Toronto

Jasmin Blanchette (August 2015)

Inria Nancy - Grand-Est, VeriDis group

Florian Rabe (June 2015)

Jacobs University Bremen, Kwarc research group

Frode Bjørdal (May 2015)

University of Oslo, Department of Philosophy

Tomer Libal (April 2015)

Ecole Polytechnique, Inria

Carsten Schürmann (April 2015)

University of Copenhagen

Aart Middeldorp (March 2015)

University of Innsbruck, Institute of Computer Science

Chad Brown (October 2014)

Saarland University, Programming Systems Lab

Geoff Sutcliffe (July 2014)

University of Miami, Department of Computer Science

The following classes are related to this project and were held at Freie Universität Berlin:

1. Winter 16: Higher-Order Theorem Proving (Alexander Steen, Max Wisniewski)
2. Summer 16: Künstliche Intelligenz (Raul Rojas, Christoph Benzmüller)
3. Summer 16: Computational Metaphysics (Christoph Benzmüller, Alexander Steen, Max Wisniewski)
4. Summer 15: Künstliche Intelligenz (Raul Rojas, Christoph Benzmüller)
5. Summer 15: Proseminar Logik (Christoph Benzmüller, Alexander Steen, Max Wisniewski)
6. Winter 14/15: Expressive Logiken -- Theorie, Mechanisierung, Anwendungen (Christoph Benzmüller, Alexander Steen, Max Wisniewski)
7. Winter 14/15: Modelchecking (Marcel Kyas)
8. Winter 13/14: Expressive Klassische und Nichtklassische Logiken und deren Automatisierung (Christoph Benzmüller)
9. Winter 13/14: Logik erster Stufe --- Theorie und Praxis (Christoph Benzmüller)

Links to similar or related projects:

• LeoPARD: Leo-III's Parallel Architecture and Datastructures (LeoPARD) is a generic system platform for implementing knowledge representation and reasoning tools (such as automated theorem prover) based on classical higher-order logic.
• LEO-II prover: A Higher-Order Theorem Prover
• Isabelle: An interactive proof assistant
• TPTP: The TPTP infrastructure