##  [Knuth–Bendix-Vervollständigung](/de/node/62346) 

 Definition

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.

 

 

 

 

 

 





## Prinzip

Prinzip

Wähle eine wohlgegründete, reduktionskompatible Ordnung auf Termen oder Wörtern, orientiere Relationen konsistent in Umformungsregeln, berechne kritische Paare (Überlappungen linker Seiten) und füge geeignete Konsequenzen als neue Regeln hinzu; iteriere, bis Konfluenz erreicht ist oder die Regelgenerierung nicht terminiert.

 

 

 

 

 





## Demonstration

Demonstration

Beginnt man mit einer Präsentation eines Monoids mit Erzeugern und definierenden Relationen, so orientiert man diese Relationen nach einer lexikographischen oder Länge-plus-Lex-Ordnung, berechnet Überlappungen zwischen Regeln zur Bestimmung kritischer Paare, reduziert diese Paare und führt neue Regeln ein, wenn die Reduktionen auseinanderlaufen; in einfachen Fällen ergibt sich so ein endliches, konfluent System mit eindeutigen Normalformen für Wörter.

 

 

 

 

## Fehlanwendung

Fehlanwendung

Zu glauben, die Vervollständigung ende immer oder das erzeugte Umformungssystem sei minimal; bei vielen nichttrivialen Präsentationen kann der Algorithmus unendlich laufen, von der Wahl der Ordnung abhängen oder redundante bzw. ineffiziente Regelmengen erzeugen, wenn kein Beschneiden erfolgt.

 

 

 

 

 





## Konsequenz

Konsequenz

Bei Erfolg liefert die Knuth–Bendix-Vervollständigung ein konfluent Umformungssystem und damit ein praktisches Entscheidungsverfahren für das Wortproblem in der präsentierten Struktur durch Reduktion auf eindeutige Normalformen; sie macht außerdem algebraische Konsequenzen der Relationen in berechenbarer Form sichtbar.

 

 

 

 

## Umkehrung

Umkehrung

Anstatt Konsequenzen hinzuzufügen, um Konfluenz zu erzwingen, könnte man Relationen entfernen oder schwächen, um leichter ein terminierendes System zu erhalten; dies kehrt das Ziel von Vervollständigung zu Approximation oder konservativer Vereinfachung um, zulasten der Korrektheit gegenüber der ursprünglichen Präsentation.

 

 

 

 

 





## Abgrenzung

Abgrenzung

Die Anwendbarkeit hängt von der Klasse der Präsentationen, der Wahl der Termordnung und der Bereitschaft, Nichtterminierung zu akzeptieren, ab; Ergebnisse sind empfindlich gegenüber nichtkommutativen versus kommutativen Rahmen und der Existenz von Identitäten, die unendlich viele kritische Paare erzeugen.

 

 

 

 

 





## Semantische Spannung

Semantische Spannung

Knuth–Bendix-Vervollständigung versus Gröbner-Basen-Methoden: Beide entfernen Redundanzen, indem sie Relationserzeuger in kanonische Formen überführen, arbeiten jedoch in unterschiedlichen algebraischen Kontexten (Umformungssysteme versus Polynomideale) mit unterschiedlichen Terminations- und Ordnungsfragen.

 

 

 

 

 





## Synthese

Synthese

Knuth–Bendix-Vervollständigung orientiert iterativ Relationen in Umformungsregeln und löst Überlappungen, um ein konfluent System zu konstruieren; als algorithmische Brücke von Präsentation zu kanonischen Normalformen ergibt sie entweder ein effektives Entscheidungsverfahren für Wortgleichheit oder zeigt durch Nichtterminierung und Ordnungsabhängigkeit die Grenzen einer solchen Reduktion auf.