Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2605.20054 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866917511515078656 |
|---|---|
| author | Chaudhuri, Kaustuv Gantait, Arunava Miller, Dale |
| author_facet | Chaudhuri, Kaustuv Gantait, Arunava Miller, Dale |
| contents | Treating syntactic equality as a logical connective -- governed by left- and right-introduction rules within the sequent calculus -- offers an elegant and powerful approach to term identity. This treatment of equality allows for the derivation of core mathematical principles, such as Peano's axioms (excluding induction), and serves as a foundation for the Abella interactive proof assistant. However, integrating this equality into automated proof search remains challenging. We present a proof search procedure that extends unification to handle the complexities of quantifier alternation and equations that occur in both positive and negative occurrences. While established logical frameworks such as $λ$Prolog and LF lack direct support for this kind of equality, our procedure enables a lightweight logical framework that addresses this gap. Our system enables unification-aware proof search across a diverse range of first-order sequent calculi that can directly use this form of equality. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_20054 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Automating proof search when equality is a logical connective Chaudhuri, Kaustuv Gantait, Arunava Miller, Dale Logic in Computer Science F.4.2 Treating syntactic equality as a logical connective -- governed by left- and right-introduction rules within the sequent calculus -- offers an elegant and powerful approach to term identity. This treatment of equality allows for the derivation of core mathematical principles, such as Peano's axioms (excluding induction), and serves as a foundation for the Abella interactive proof assistant. However, integrating this equality into automated proof search remains challenging. We present a proof search procedure that extends unification to handle the complexities of quantifier alternation and equations that occur in both positive and negative occurrences. While established logical frameworks such as $λ$Prolog and LF lack direct support for this kind of equality, our procedure enables a lightweight logical framework that addresses this gap. Our system enables unification-aware proof search across a diverse range of first-order sequent calculi that can directly use this form of equality. |
| title | Automating proof search when equality is a logical connective |
| topic | Logic in Computer Science F.4.2 |
| url | https://arxiv.org/abs/2605.20054 |