Automating proof search when equality is a logical connective

Kaustuv Chaudhuri, Arunava Gantait, Dale Miller

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…