Editing Knuth–Bendix completion algorithm (section)

===Description of the algorithm for finitely presented monoids===

Suppose we are given a [[presentation of a group|presentation]] <math> \langle X \mid R \rangle </math>, where <math> X </math> is a set of [[generating set of a group|generator]]s and <math> R </math> is a set of [[Relation (mathematics)|relations]] giving the rewriting system.  Suppose further that we have a reduction ordering <math> < </math> among the words generated by <math> X </math>(e.g., [[shortlex order]]).  For each relation <math> P_i = Q_i </math> in <math> R </math>, suppose <math> Q_i < P_i </math>.  Thus we begin with the set of reductions <math> P_i \rightarrow Q_i </math>.

First, if any relation <math> P_i = Q_i </math> can be reduced, replace <math> P_i </math> and <math> Q_i </math> with the reductions.

Next, we add more reductions (that is, rewriting rules) to eliminate possible exceptions of confluence.  Suppose that <math> P_i </math> and <math> P_j </math> overlap.

# Case 1: either the prefix of <math> P_i</math> equals the suffix of <math> P_j </math>, or vice versa.  In the former case, we can write <math> P_i = BC </math> and <math> P_j = AB </math>; in the latter case, <math> P_i = AB </math> and <math> P_j = BC </math>.
#Case 2: either <math> P_i</math> is completely contained in (surrounded by)  <math> P_j </math>, or vice versa. In the former case, we can write <math> P_i = B </math> and <math> P_j = ABC </math>; in the latter case, <math> P_i = ABC </math> and <math> P_j = B </math>.

Reduce the word <math> ABC </math> using <math> P_i </math> first, then using <math> P_j </math> first.  Call the results <math> r_1, r_2 </math>, respectively.  If <math> r_1 \neq r_2 </math>, then we have an instance where confluence could fail.  Hence, add the reduction <math> \max r_1, r_2 \rightarrow \min r_1, r_2 </math> to <math> R </math>.

After adding a rule to <math> R </math>, remove any rules in <math> R </math> that might have reducible left sides (after checking if such rules have critical pairs with other rules).

Repeat the procedure until all overlapping left sides have been checked.