Automating proof search when equality is a logical connective

TL;DR

This paper introduces a proof search procedure that extends unification to handle equality as a logical connective, facilitating automated reasoning in sequent calculus frameworks.

Contribution

It presents a novel proof search method that integrates equality as a logical connective into automated proof search, addressing limitations in existing logical frameworks.

Findings

Enables unification-aware proof search with equality in first-order sequent calculi.

Extends unification to handle quantifier alternation and equations in positive and negative contexts.

Supports a lightweight logical framework for automated reasoning with equality.

Abstract

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