Optimistic Higher-Order Superposition

TL;DR

This paper introduces an optimistic variant of the lambda-superposition calculus that delays complex unification and applies extensionality more selectively, aiming to improve higher-order theorem proving efficiency.

Contribution

It proposes a new calculus that mitigates explosion issues in higher-order unification and extensionality, maintaining soundness and completeness under Henkin semantics.

Findings

The new calculus is sound and refutationally complete.

Examples suggest potential performance improvements over the original calculus.

The approach delays unification problems using constraints.

Abstract

The $\lambda$-superposition calculus is a successful approach to proving higher-order formulas. However, some parts of the calculus are extremely explosive, notably due to the higher-order unifier enumeration and the functional extensionality axiom. In the present work, we introduce an "optimistic" version of $\lambda$-superposition that addresses these two issues. Specifically, our new calculus delays explosive unification problems using constraints stored along with the clauses, and it applies functional extensionality in a more targeted way. The calculus is sound and refutationally complete with respect to a Henkin semantics. We have yet to implement it in a prover, but examples suggest that it will outperform, or at least usefully complement, the original $\lambda$-superposition calculus.