Leo IIIP.Leo III

Freie Universität Berlin

Leo III - A Massively Parallel Higher-Order Theorem Prover

Overview

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).

People

Leo III is currently being developed by

with contributions from

Further collaborators:

  • Frank Theiss
  • Leon Weber
  • Daniel Jentsch

Downloads

Leo-III Downloads

The first public version of Leo-III will be reased in summer 2017 together with its entry at CASC-26.

Related Downloads
  • Capability descriptions of the ATP systems
  • 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.

Core Project Publications

  1. Christoph Benzmüller, Alexander Steen, Max Wisniewski Leo-III Version 1.1 (System description), In Thomas Eiter, David Sands (Eds.), Logic for Programming, Artificial Intelligence, and Reasoning (LPAR) -- Short Presentations, EasyChair, Kalpa Publications, 2017. (To appear)
  2. 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.
  3. 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.
  4. 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.
  5. 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.
  6. Max Wisniewski, Agent-based Blackboard Architecture for a Higher-Order Theorem Prover. Master Thesis, Freie Universität Berlin, revised version, 2014.
  7. Alexander Steen, Efficient Data Structures for Automated Theorem Proving in Expressive Higher-Order Logics. Master Thesis, Freie Universität Berlin, revised version, 2014.
  8. Max Wisniewski, Alexander Steen, Christoph Benzmüller, The Leo-III Project. In Alexander Bolotov, Manfred Kerber (eds.), Joint Automated Reasoning Workshop and Deduktionstreffen, 2014.
  9. 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.

Related Publications

  • Tobias Gleißner, Alexander Steen, Christoph Benzmüller, Theorem Provers for Every Normal Modal Logic, In Thomas Eiter, David Sands (Eds.), Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), EasyChair, EPiC Series in Computing, 2017. (To appear)
  • 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 2nd International Workshop on Automated Reasoning in Quantified Non-Classical Logics, (ARQNL 2016), Coimbra, Portugal, July 2016, Proceedings, EasyChair, EasyChair Proceedings in Computing.
  • 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.

Guests and Invited Talks

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

Permanent guests

Hans-Jörg Schurr (since October 2015)
TU Wien

Related Teaching Activities

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