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