Kongruenzabschluss‑Algorithmus

Ein algorithmisches Verfahren, das zu einer gegebenen Menge von Gleichungen über Grundterme (oder Terme in einer Signatur) die kleinste Kongruenzrelation berechnet, die diese Gleichungen enthält — also die geringste Äquivalenz, die unter Anwendung von Funktionssymbolen abgeschlossen ist — zur Entscheidung von äquationaler Folgerung.