Optimistic Higher-Order Superposition
Alexander Bentkamp, Jasmin Blanchette, Matthias Hetzenberger, Uwe Waldmann
TL;DR
This work introduces an optimistic variant of the $\lambda$-superposition calculus for higher-order logic that mitigates two major sources of combinatorial explosion: explosive higher-order unifier enumeration and aggressive extensionality reasoning. It achieves this by (i) delaying unification problems with constraints attached to clauses, and (ii) applying a targeted functional extensionality rule in concert with bespoke term orders. The authors prove soundness and refutational completeness with respect to Henkin semantics, and outline a six-level completeness framework that connects higher-order constrained clauses to first-order encodings. While not yet implemented, the approach is motivated by practical provers like Vampire and is designed to be empirically competitive, with stronger redundancy criteria aiding clause simplification. The framework also clarifies how to encode higher-order reasoning into a first-order setting and how to manage constraints and parameters across multiple abstraction levels.
Abstract
The $λ$-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 $λ$-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 $λ$-superposition calculus.