J. Avenhaus, Th. Hillenbrand, B. Löchner
Beim Einsatz von Termersetzungs- und Vervollständigungstechniken für das Gleichheitsbeweisen wird die Menge der Axiome saturiert mit dem Zweck, ein terminierendes und auf Grundtermen konfluentes Reduktionssystem zu erhalten. Dieses sollte einerseits eine starke Simplifikationsrelation etablieren, andererseits möglichst wenige kritische Paare erzeugen, um den Berechnungsaufwand gering zu halten. Im Falle assoziativ-kommutativer (AC) Operatoren ist dies schwierig, da eine permutative Vielfalt aufgezählt wird.
Wir zeigen, wie diese beiden Ziele in einem gewissen Ausmaß erreicht werden können, indem grundzusammenführbare Gleichungen zum Simplifizieren verwendet werden, allerdings nicht zum Generieren kritischer Paare. Die Vollständigkeit des Verfahrens bleibt dabei erhalten. Für den Spezialfall von AC-Operatoren geben wir ein Kriterium an, welches einfach effizient zu implementieren ist und sich in der Praxis als sehr effektiv erweist