# Extensional Higher-Order Paramodulation in Leo-III

## TL;DR

Leo-III is an advanced automated theorem prover that handles extensional higher-order logic with primitive equality, supporting cooperation with various reasoning systems and extending the TPTP framework to non-classical logics.

## Contribution

It introduces extensional higher-order paramodulation in Leo-III, enabling reasoning in complex logics and integration with external systems, advancing the TPTP infrastructure.

## Key findings

- Supports reasoning in polymorphic first-order and higher-order logic
- Enables cooperation with external provers and SMT solvers
- Extends TPTP infrastructure for non-classical logics

## Abstract

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.