@online{Bentkamp2510.18429,
TITLE = {Optimistic Higher-Order Superposition},
AUTHOR = {Bentkamp, Alexander and Blanchette, Jasmin and Hetzenberger, Matthias and Waldmann, Uwe},
URL = {https://arxiv.org/abs/2510.18429},
EPRINT = {2510.18429},
EPRINTTYPE = {arXiv},
YEAR = {2025},
MARGINALMARK = {$\bullet$},
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.},
}