The $\lambda$-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 $\lambda$-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 $\lambda$-superposition calculus.

翻译：$\lambda$-叠加演算是证明高阶公式的一种成功方法。然而，该演算的某些部分具有极高的爆炸性，这主要源于高阶合一器的枚举以及函数外延性公理。在当前工作中，我们提出了一种“乐观”版本的$\lambda$-叠加演算，以解决这两个问题。具体而言，我们的新演算通过将约束条件与子句一同存储，从而延迟处理爆炸性的合一问题，并以更具针对性的方式应用函数外延性。该演算相对于亨金语义是可靠且反驳完备的。我们尚未在证明器中实现它，但示例表明，其性能将优于或至少能有效补充原始的$\lambda$-叠加演算。