Ansatzpunkte für heuristische Methoden bei der Vervollständigung

Abstract

We deal with the most important features of the Knuth-Bendix completion procedure considered as search problems. There are four indeterminisms in this algorithm: ordering, computation of normalforms, interreduction and selection of critical pairs. They are represented as search trees in order to show the programmer's choices when implementing such an algorithm. The problems are outlined by examples and some possible heuristic criteria for their solutions are given.

Wir betrachten den Knuth-Bendix-Vervollständigungsalgorithmus unter dem Aspekt von Suchproblemen. Die vier Indeterminismen: Ordnung, Normalformbildung, Interreduction und Auswahl des nächsten kritischen Paares werden als Suchbäume uniform dargestellt, um die Wahlmöglichkeiten eines Programmierers bei dem Implementation einer Vervollständigung aufzuzeigen. Die auftretenden Probleme werden an Hand von Beispielen geschildert und Ansatzpunkte für Heuristiken zur Lösung dieser Probleme gegeben.