The Knuth-Bendix completion algorithm attempts to transform a finite set of identities into a finitely terminating, confluentterm 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: . 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 algorithm provided that every identity
is viewed as two candidates for rewrite rules transforming the left-hand side into
the right-hand side and vice versa.

The output term rewriting system is used to determine whether is an identity or not in the following manner. If two distinct
terms
and
have the same normal form, then is an identity. Otherwise, is not an identity. Term rewriting systems that are both
finitely terminating and confluent
enjoy the property of having unique normal forms for all expressions. The problem
of deciding whether is an identity is also known as the word problem.

Initially, this algorithm attempts to orient input identities according to the reduction order (if, then becomes a rule). Then, it completes this initial set
of rules with derived ones. The algorithm iteratively detects critical
pairs, obtains their normal forms, and adds a new rule for every pair of the
normal forms in accordance with the reduction order.

This algorithm may

1. Terminate with success and yield a finitely terminating, confluent set of rules,

Baader, F. and Nipkow, T. Term Rewriting and All That. Cambridge, England: Cambridge University Press, 1999.Knuth
D. E. and Bendix P. B. "Simple Word Problems in Universal Algebra."
In Computational Problems in Abstract Algebra (Proc. Conf., Oxford, 1967).
Pergamon Press, pp. 263-297, 1970.Wolfram, S. A
New Kind of Science. Champaign, IL: Wolfram Media, p. 1037,
2002.