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.
BibTeX
@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.},
}Endnote
%0 Report %A Bentkamp, Alexander %A Blanchette, Jasmin %A Hetzenberger, Matthias %A Waldmann, Uwe %+ External Organizations External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T Optimistic Higher-Order Superposition : %U http://hdl.handle.net/21.11116/0000-0012-5905-3 %U https://arxiv.org/abs/2510.18429 %D 2025 %X 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. %K Computer Science, Logic in Computer Science, cs.LO,Computer Science, Artificial Intelligence, cs.AI