Term rewriting for equational theories

Summary

Term rewriting replaces the symmetric equations of an equational theory by one-way rules $l \to r$ that rewrite terms. Two terms are equal in the theory exactly when they are connected by a chain of rule applications in either direction. When the rules are terminating and confluent, every term has a unique normal form. Then two terms are equal in the theory exactly when their normal forms coincide. This turns many word problems for free algebras into a mechanical computation, and the Knuth–Bendix procedure tries to find such rules.