Adventures in sequent calculus modulo equations
Abstract 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.