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: 
. 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,
2. Terminate with failure, or
3. Loop without terminating.
Note that Buchberger's algorithm for constructing Gröbner bases is very similar to the Knuth-Bendix completion algorithm.
