 Equality is an important logical relation whose behavior within automated deduction deserves its own separate treatment. Equational logic and, more generally, term rewriting treat equality-like equations as rewrite rules, also known as reduction or demodulation rules. An equality statement like f(a)= a allows the simplification of a term like g(c,f(a)) to g(c,a). However, the same equation also has the potential to generate an unboundedly large term: g(c,f(a)), g(c,f(f(a))), g(c,f(f(f(a)))), … . What distinguishes term rewriting from equational logic is that in term rewriting equations are used as unidirectional reduction rules as opposed to equality which works in both directions. Rewrite rules have the form t1 ⇒ t2 and the basic idea is to look for terms t occurring in expressions e such that t unifies with t1 with unifier θ so that the occurrence t1θ in eθ can be replaced by t2θ. For example, the rewrite rule x + 0 ⇒ x allows the rewriting of succ(succ(0) + 0) as succ(succ(0)).