ein Algorithmus für das Wortproblem in universellen Algebren, ähnlich dem Buchberger-Algorithmus aufgebaut.

Einer Menge F von Identitäten wird mit Hilfe des Algorithmus eine Standardbasis zugeordet, mit deren Hilfe man für einen gegebenen Term eine Normalform berechnen kann. Zwei Terme sind modulo der Identitäten gleich, wenn ihre Normalformen identisch sind.