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