Term Rewriting System
Term rewriting systems are reduction systems in which rewrite rules apply to terms. Terms are built up
from variables and constants using function symbols (or operations). Rules of term
rewriting systems have the form 
, where both
and 
are terms, 
is not a variable, and every variable from 
occurs in 
as well.
A reduction step for term 
is defined as follows.
If 
is a unifier
for 
and 
, then 
is reduced to 
. If 
is a unifier
for 
and 
where 
is a subterm
of 
, then 
is reduced to a
term obtained from 
by replacing
with 
.
Contact the MathWorld Team
{{2,3},{4,5}}^(-1)