# Optimistic Higher-Order Superposition

arXiv: https://arxiv.org/abs/2510.18429 · HTML: https://mlsanity.com/paper/2510.18429/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- First posted on arXiv 21 Oct 2025.

## Abstract (arXiv)

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.