Extensional Higher-Order Paramodulation in Leo-III
This work addresses the need for automated theorem proving in non-classical logics, such as modal and deontic logics, for researchers and practitioners in formal verification and logic, and is incremental as it builds on existing paramodulation methods and extends the TPTP infrastructure.
The paper tackles the problem of automated theorem proving in extensional type theory by adapting paramodulation-based proof search to higher-order logic, resulting in Leo-III, a prover that supports reasoning in polymorphic first-order and higher-order logic, all normal quantified modal logics, and different deontic logics, and is compatible with the TPTP/TSTP framework.
Leo-III is an automated theorem prover for extensional type theory with Henkin semantics and choice. Reasoning with primitive equality is enabled by adapting paramodulation-based proof search to higher-order logic. The prover may cooperate with multiple external specialist reasoning systems such as first-order provers and SMT solvers. Leo-III is compatible with the TPTP/TSTP framework for input formats, reporting results and proofs, and standardized communication between reasoning systems, enabling e.g. proof reconstruction from within proof assistants such as Isabelle/HOL. Leo-III supports reasoning in polymorphic first-order and higher-order logic, in all normal quantified modal logics, as well as in different deontic logics. Its development had initiated the ongoing extension of the TPTP infrastructure to reasoning within non-classical logics.