Equality reasoning in sequent-based calculi (Q2751362)

The authors present a review of automated reasoning techniques for all main sequent-based methods of automated reasoning. The paper covers the following topics: NEWLINENEWLINENEWLINE-- methods of proof-search in sequent-based calculi, NEWLINENEWLINENEWLINE-- translation of logic with equality into logic without equality,NEWLINENEWLINENEWLINE-- theorem proving using simultaneous \(E\)-unification,NEWLINENEWLINENEWLINE-- tableau calculi with rigid paramodulation and superposition,NEWLINENEWLINENEWLINE-- the equality elimination method,NEWLINENEWLINENEWLINE-- equality reasoning in nonclassical logic.NEWLINENEWLINENEWLINEThe paper contains a voluminous bibliography concerning the considered topics.NEWLINENEWLINEFor the entire collection see [Zbl 0964.00020].