Optimistic Higher-Order Superposition
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.
Cite
@article{arxiv.2510.18429,
title = {Optimistic Higher-Order Superposition},
author = {Alexander Bentkamp and Jasmin Blanchette and Matthias Hetzenberger and Uwe Waldmann},
journal= {arXiv preprint arXiv:2510.18429},
year = {2025}
}