Leo-III – Effective Automation for Higher-Order Logic
Leo-III was funded by DFG under grant BE 2501/11-1 (Leo-III), PI: C. Benzmüller
Leo-III is an effective ATP system for HOL with Henkin semantics and choice.
It is implemented in Scala; its source code, and that of related projects, is publicly
available under BSD-3 license on GitHub. The system accepts all common
TPTP input
syntax formats, including untyped clause normal form (CNF), untyped and typed first-order
logic (FOF and TFF, respectively) and, as primary input format, monomorphic higher-order
logic (THF). Additionally, as one of the first higher-order ATP systems, Leo-III
upports reasoning in rank-1 polymorphic variants of the above logics (TF1 and TH1 syntax).
The prover returns results according to the standardized TPTP SZS ontology and
produces a verifiable TPTP-compatible proof certificate, if a proof is found.
Leo-III was identified as one of the most effective (in terms of number of solved
problems) and most versatile (in terms of supported logical formalisms) theorem prover
to date by the GRUNDE evaluation. Also. Leo-III won the LTB division of the CASC-27 in 2019.
Further information
-
Leo-III @ GitHub: Code of and instructions for Leo-III are available at
github.com/leoprover/Leo-III.
-
Leo-III example input and outputs: Case studies for the application of Leo-III
to higher-order logic problems, modal logic reasoning, choice reasoning and polymorphic HOL
reasoning are available as supplemental material to my PhD thesis.
-
Dissertation abstract about Leo-III: A 4-page overview of the Leo-III
project and its theoretical and practical details is freely avaiable at
Springer Link.
MET – Modal Embedding Tool for Reasoning in Quantified Modal Logics
Conducted at Dahlem Center of Machine Learning and Robotics of Freie Universität Berlin,
joint work with T. Gleißner
MET is a tool for embedding modal logic logic problems into classical higher-order logic
represented in TPTP THF format. The input language allows the user to specify the semantics
of the desired quantified modal logic and automatically computes the correspondig
embedding.
Further information
-
MET @ GitHub: Code of and instructions for MET are available at
github.com/leoprover/embed_modal.
-
Ongoing standardization project as TPTP standard:
The input format is currently considered as a logic specification format standard at the
TPTP infrastructure, see the
proposal document.
NAI – Normative Reasoning/Legal Analysis
Conducted at the Individual and Collective Reasoning group of University of Luxembourg,
joint work with T. Libal
NAI (for Normative AI) is a framework for normative reasoning. NAI features an annotation-based
editor which abstracts over the underlining logical language.
It also contains an easily accessible functionality for quality assurance and a transparent
analysis of the created formalized document. NAI also supports an approach for
assessing the correctness of formalizations via execution of behavioral tests
using so-called queries. Lastly, it provides an interface for the creation of such
queries and for checking their validity. The architecture of NAI is modular, which
allows using different logics and reasoning engines. It also provides an web-based
interface, which can be used by other tools in order to reason over the formalized legislation.
NAI is open-source, its source code is freely available at GitHub 3 under GPL-3.0 license.
It was awarded with the LexisNexis Best Paper Award of Internationales Rechtsinformatik
Symposium (IRIS 2020), in Salzburg, Austria, 2020.
Further information
-
NAI @ GitHub: Code of and instructions for the frontend and backend of NAI are available at
github.com/normativeai.
-
NAI web tool: An instance of NAI is hosted at
nai.uni.lu, free for own experimentation and tests.
-
Tutorial material: Tutorial material that was used in lectures on
normative reasoning at the
ICAIL 2019 conference in Montreal, Canada, is available at tutorial.normativeai.com.
-
Youtube video tutorial for NAI: A visual guide by Tomer Libal
for the usage of NAI can be found at Youtube.
It was presented by Tomer at ReMeP 2019.
0000-0001-8781-9462