Knuth-Bendix Completion Algorithm -- from Wolfram MathWorld

The Knuth-Bendix completion algorithm attempts to transform a finite set of identities into a finitely terminating, confluent term rewriting system whose reductions preserve identity. This term rewriting system serves a decision procedure for validating identities. As defined in universal algebra, identities are equalities of two terms: x=y. Presumably, the values of the two terms are equal for all values of variables occurring in them. A reduction order is another input to the completion...