Editing Knuth–Bendix completion algorithm (section)

==Example==

The following example run, obtained from the [[E theorem prover]], computes a completion of the (additive) group axioms as in Knuth, Bendix (1970).
It starts with the three initial equations for the group (neutral element 0, inverse elements, associativity), using <code>f(X,Y)</code> for ''X''+''Y'', and <code>i(X)</code> for −''X''. 
The 10 starred equations turn out to constitute the resulting convergent rewrite system.
"pm" is short for "[[Resolution (logic)#Paramodulation|paramodulation]]", implementing ''deduce''. Critical pair computation is an instance of paramodulation for equational unit clauses.
"rw" is rewriting, implementing ''compose'', ''collapse'', and ''simplify''.
Orienting of equations is done implicitly and not recorded.
{| class=wikitable
|-
| '''Nr''' || || ALIGN=RIGHT | '''Lhs''' || || '''Rhs''' || '''Source'''
|-
| 1:    || <sup>*</sup> || ALIGN=RIGHT | f(X,0)                 || =    || X                    || initial("GROUP.lop", at_line_9_column_1)
|-
| 2:    || <sup>*</sup> || ALIGN=RIGHT | f(X,i(X))              || =    || 0                    || initial("GROUP.lop", at_line_12_column_1)
|-
| 3:    || <sup>*</sup> || ALIGN=RIGHT | f(f(X,Y),Z)            || =    || f(X,f(Y,Z))          || initial("GROUP.lop", at_line_15_column_1)
|-
| 5:    ||              || ALIGN=RIGHT | f(X,Y)                 || =    || f(X,f(0,Y))          || pm(3,1)
|-
| 6:    ||              || ALIGN=RIGHT | f(X,f(Y,i(f(X,Y))))    || =    || 0                    || pm(2,3)
|-
| 7:    ||              || ALIGN=RIGHT | f(0,Y)                 || =    || f(X,f(i(X),Y))       || pm(3,2)
|-
| 27:   ||              || ALIGN=RIGHT | f(X,0)                 || =    || f(0,i(i(X)))         || pm(7,2)
|-
| 36:   ||              || ALIGN=RIGHT | X                      || =    || f(0,i(i(X)))         || rw(27,1)
|-
| 46:   ||              || ALIGN=RIGHT | f(X,Y)                 || =    || f(X,i(i(Y)))         || pm(5,36)
|-
| 52:   || <sup>*</sup> || ALIGN=RIGHT | f(0,X)                 || =    || X                    || rw(36,46)
|-
| 60:   || <sup>*</sup> || ALIGN=RIGHT | i(0)                   || =    || 0                    || pm(2,52)
|-
| 63:   ||              || ALIGN=RIGHT | i(i(X))                || =    || f(0,X)               || pm(46,52)
|-
| 64:   || <sup>*</sup> || ALIGN=RIGHT | f(X,f(i(X),Y))         || =    || Y                    || rw(7,52)
|-
| 67:   || <sup>*</sup> || ALIGN=RIGHT | i(i(X))                || =    || X                    || rw(63,52)
|-
| 74:   || <sup>*</sup> || ALIGN=RIGHT | f(i(X),X)              || =    || 0                    || pm(2,67)
|-
| 79:   ||              || ALIGN=RIGHT | f(0,Y)                 || =    || f(i(X),f(X,Y))       || pm(3,74)
|-
| 83:   || <sup>*</sup> || ALIGN=RIGHT | Y                      || =    || f(i(X),f(X,Y))       || rw(79,52)
|-
| 134:  ||              || ALIGN=RIGHT | f(i(X),0)              || =    || f(Y,i(f(X,Y)))       || pm(83,6)
|-
| 151:  ||              || ALIGN=RIGHT | i(X)                   || =    || f(Y,i(f(X,Y)))       || rw(134,1)
|-
| 165:  || <sup>*</sup> || ALIGN=RIGHT | f(i(X),i(Y))           || =    || i(f(Y,X))            || pm(83,151)

|}
See also [[Word problem (mathematics)]] for another presentation of this example.