Optimistic Higher-Order Superposition
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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Superposition with Lambdas
We designed a superposition calculus for a clausal fragment of extensional polymorphic higher-order logic that includes anonymous functions but excludes Booleans. The inference rules work on $\beta\eta$-equivalence class…
Superposition for Lambda-Free Higher-Order Logic
We introduce refutationally complete superposition calculi for intentional and extensional clausal $\lambda$-free higher-order logic, two formalisms that allow partial application and applied variables. The calculi are p…
Superposition with Delayed Unification
Classically, in saturation-based proof systems, unification has been considered atomic. However, it is also possible to move unification to the calculus level, turning the steps of the unification algorithm into inferenc…
SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning
We show that SCL(FOL) can simulate the derivation of non-redundant clauses by superposition for first-order logic without equality. Superposition-based reasoning is performed with respect to a fixed reduction ordering. T…
Generalized Optimistic Methods for Convex-Concave Saddle Point Problems
The optimistic gradient method has seen increasing popularity for solving convex-concave saddle point problems. To analyze its iteration complexity, a recent work [arXiv:1906.01115] proposed an interesting perspective th…
Second-order methods