The Higher-Order Prover Leo-III (Extended Version)

TL;DR

Leo-III is a versatile higher-order theorem prover supporting various logics and dialects, offering proof certificates and demonstrating strong performance on diverse benchmarks.

Contribution

This paper introduces Leo-III, a new higher-order theorem prover with support for multiple logics, dialects, and proof certification, extending prior tools in scope and capabilities.

Findings

Supports all common TPTP dialects including recent extensions

Cooperates with first-order tools via translations

Performs well on heterogeneous benchmark sets

Abstract

The automated theorem prover Leo-III for classical higher-order logic with Henkin semantics and choice is presented. Leo-III is based on extensional higher-order paramodulation and accepts every common TPTP dialect (FOF, TFF, THF), including their recent extensions to rank-1 polymorphism (TF1, TH1). In addition, the prover natively supports almost every normal higher-order modal logic. Leo-III cooperates with first-order reasoning tools using translations to many-sorted first-order logic and produces verifiable proof certificates. The prover is evaluated on heterogeneous benchmark sets.