改进高阶合一与函数外延性，让高阶自动推理更高效
Optimistic Higher-Order Superposition
- 用约束延迟爆炸性合一问题，避免过早展开
- 仅在必要时应用函数外延性，减少无效推导
- 理论完备且适合高阶逻辑证明器优化
λ-超位置演算是一种成功的高阶公式证明方法。但其部分机制极容易引发计算爆炸，尤其源于高阶合一枚举和函数外延性公理。本文提出一种‘乐观’版本的λ-超位置，通过在子句中存储约束来延迟爆炸性合一问题，并更精准地应用函数外延性。该演算在亨金语义下保持正确性和反证完备性。虽尚未在证明器中实现，但实例表明其性能有望优于或至少可有效补充原版λ-超位置演算。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。