Vervollständigung: Knuth/Bendix, 1970

• Donald Knuth and Peter Bendix: Word Problems in Universal Algebras 1970
• E sind Gruppen-Axiome, Signatur {e/0, i/1, m/2}
  1. m(e(), x)→x
  2. m(i(x), x)→e()
  3. m(m(x, y), z)→m(x, m(y, z))
  abgeleitet z.B.: 8. m(x, e())→x
• kritische Paare wie hier definiert, orientiert nach der (später so benannten) Knuth-Bendix-Ordnung (KBO):
  • abnehmende Summe von Buchstabengewichten ∈$\mathbb {N}$
  • bei gleicher Summe: lexikogr. Abstieg bzgl. > auf Σ
  • Vorsicht bei Gewichten 0, damit SN( > _KBO)