Adventures in sequent calculus modulo equations
Patrick Viry · Electronic Notes in Theoretical Computer Science · 1998
We apply the notion of an oriented rewrite theory and the associated coherence techniques in order to construct a framework for theorem proving modulo equations. This is achieved using existing rewriting techniques and a few simple lemmas, and is intended to serve as a case study of the use of an oriented rewrite theory for building-in equality.