Optimistic Higher-Order Superposition
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914105197068288 |
|---|---|
| author | Bentkamp, Alexander Blanchette, Jasmin Hetzenberger, Matthias Waldmann, Uwe |
| author_facet | Bentkamp, Alexander Blanchette, Jasmin Hetzenberger, Matthias Waldmann, Uwe |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2510_18429 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Optimistic Higher-Order Superposition Bentkamp, Alexander Blanchette, Jasmin Hetzenberger, Matthias Waldmann, Uwe Logic in Computer Science Artificial Intelligence I.2.3 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. |
| title | Optimistic Higher-Order Superposition |
| topic | Logic in Computer Science Artificial Intelligence I.2.3 |
| url | https://arxiv.org/abs/2510.18429 |