Term Rewriting System

Term Rewriting System -- from Wolfram MathWorld

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 .