2025/10/21 by Alexander Bentkamp, Bentkamp, Alexander, Jasmin Christian Blanchette +5
Computer Science · #Artificial Intelligence (cs.AI) #FOS: Computer and information sciences #Formal Methods in Verification #I.2.3 #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2510.18429
openalex publication_date 2025/10/21 · openalex created_date 2025/10/24 · openalex updated_date 2026/07/28
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.