Rewrite Proofs and Computations

Rewriting is a general paradigm for expressing computations in various logics, and we focus here on rewriting techniques in equational logic. When used at the proof level, rewriting provides with a very powerful methodology for proving completeness results, a technique that is illustrated here. We also consider whether important properties of rewrite systems such as confluence and termination can be proved in a modular way. Finally, we stress the links between rewriting and tree automata.

full paper