Knuth–Bendix-Vervollständigung

Ein Verfahren, das auf ein gegebenes Umformungssystem angewandt wird und versucht, ein konfluent (vollständiges) Term-Umformungssystem zu erzeugen, indem Relationen unter einer gewählten Reduktionsordnung in Umformungsregeln orientiert und Folgen aus kritischen Überlappungen hinzugefügt werden, bis keine ungelösten kritischen Paare mehr verbleiben oder der Prozess divergiert.

Ein algorithmisches Verfahren, das eine Menge von Umschreibungsregeln (oder Relationen) und eine wohlfundierte Reduktionsordnung annimmt und versucht, die Regelmenge durch Hinzufügen von Konsequenzen (Auflösen kritischer Paare) so zu erweitern, dass ein konfluentes (und terminierendes) Umschreibungssystem entsteht, das im Erfolgsfall das Wortproblem in der präsentierten Algebra löst.