Optimistic Higher-Order Superposition
This addresses efficiency issues in automated theorem proving for higher-order logic, which is incremental as it builds on existing calculus methods.
The paper tackles the explosiveness of the λ-superposition calculus in proving higher-order formulas by introducing an 'optimistic' version that delays unification problems and applies functional extensionality more targeted, aiming to outperform or complement the original calculus.
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.