# Extensional Higher-Order Paramodulation in Leo-III

arXiv: https://arxiv.org/abs/1907.11501 · HTML: https://mlsanity.com/paper/1907.11501/

## Key facts

- Cited by 11 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 26 Jul 2019.

## Built on by (most cited first, 11 of 11)

- [Automated Reasoning in Non-classical Logics in the TPTP World](https://mlsanity.com/paper/2202.09836/) (2022)
- [An Extensible Logic Embedding Tool for Lightweight Non-Classical Reasoning](https://mlsanity.com/paper/2203.12352/) (2022)
- [Faithful Logic Embeddings in HOL -- Deep and Shallow](https://mlsanity.com/paper/2502.19311/) (2025)
- [Bridging between LegalRuleML and TPTP for Automated Normative Reasoning (extended version)](https://mlsanity.com/paper/2209.05090/) (2022)
- [Many Logics, One Methodology: A Plea for Logical Pluralism in Formalised Reasoning (preprint)](https://mlsanity.com/paper/2605.27246/) (2026)
- [A Formalisation of Abstract Argumentation in Higher-Order Logic](https://mlsanity.com/paper/2110.09174/) (2021)
- [TPTP World Infrastructure for Non-classical Logics](https://mlsanity.com/paper/2508.09318/) (2025)
- [Theorem Proving in Dependently-Typed Higher-Order Logic -- Extended Preprint](https://mlsanity.com/paper/2305.15382/) (2023)
- [An Encoding of Abstract Dialectical Frameworks into Higher-Order Logic](https://mlsanity.com/paper/2312.08375/) (2023)
- [Experiments with Choice in Dependently-Typed Higher-Order Logic](https://mlsanity.com/paper/2410.08874/) (2024)
- [Same Formulas, Different Semantics: Do Language Models Follow Modal Logic Specifications?](https://mlsanity.com/paper/2608.05097/) (2026)

## Abstract (arXiv)

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.