{"ID":2852138,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2510.18429","arxiv_id":"2510.18429","title":"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.","short_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 $λ$-superpositi...","url_abs":"https://arxiv.org/abs/2510.18429","url_pdf":"https://arxiv.org/pdf/2510.18429v1","authors":"[\"Alexander Bentkamp\",\"Jasmin Blanchette\",\"Matthias Hetzenberger\",\"Uwe Waldmann\"]","published":"2025-10-21T09:05:54Z","proceeding":"cs.LO","tasks":"[\"cs.LO\",\"cs.AI\"]","methods":"[]","has_code":false}