Term rewriting is the process of simplifying symbolic expressions (_terms_) by means of a RewriteSystem, i.e., a set of RewriteRules.
An example rewrite system is the following:
0 + x -> x
s(x) + y -> s(x + y)
(x + y) + z -> x + (y + z)
The NormalForm of the term `((s(s(a)) + s(b)) + c)`

under these rewrite rules
is the term `s(s(s(a + (b + c))))`

.
The order in which rules are applied to the term is determined by the RewritingStrategy.
*See also*
* AlgebraicSpecification
* TermRewritingImplementation
* RewritingHomePage