-
Notifications
You must be signed in to change notification settings - Fork 1
System Leo III
Christoph Benzmüller, Alexander Steen, Max Wisniewski.
Leo-III is an automated theorem prover for (polymorphic) higher-order logic. It is based on a paramodulation calculus with ordering constraints and, in tradition of its predecessor LEO-II, heavily relies on cooperation with external (mostly first-order) theorem provers for increased performance. Nevertheless, Leo-III can also be used as a stand-alone prover without employing any external cooperation. In addition for its HOL reasoning capabilities, Leo-III supports reasoning in many non-classical logics, e.g., quantified modal logics.
Leo-III is developed at Freie Universität Berlin (2014 - 2018), the University of Luxembourg (2018 - 2021) and the University of Greifswald (since 2022).
Leo-III is open-source and licensed under the BSD 3-clause "New" or "Revised" License.
- Proving
- Model finding
Leo-III supports all common TPTP dialects, including FOF, TFF, and THF as well as their rank-1 polymorphic derivatives. This corresponds to classical (unsorted and many-sorted) first-order logic and higher-order logics, respectively. Also, Leo-III supports some basic arithmetics and reasoning with choice.
Furthermore, Leo-III is the first ATP system to support the non-classical TPTP format, supporting first-order modal logics, deontic logics and epistemic logics, see the Leo-III documentation for details.
Leo-III follows the SZS reporting standard
LEO-II can output proofs in the TPTP format.
https://github.com/leoprover/Leo-III
Leo-III is written in the Scala programming language.
From 2014 - 2018, it was supported by the German National Research Foundation (DFG) under project BE 2501/11-1 (Leo-III). Leo-III may be cited with DOI 10.5281/zenodo.4435994.
Leo-III is included in the Sledgehammer tool of Isabelle/HOL.
Maintained
Alexander Steen, Christoph Benzmüller, Extensional Higher-Order Paramodulation in Leo-III. Journal of Automated Reasoning 65, pp. 775-807, 2021. DOI: 10.1007/s10817-021-09588-x. Preprint available at arXiv:1907.11501.
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. Preprint available here.