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.

Prinzip

Schließe die Eingabegleichungen unter Reflexivität, Symmetrie, Transitivität und Kongruenz: wenn a=b, dann sind für jeden Kontext f(...,a,...) und f(...,b,...) die Ergebnisse äquivalent; implementierbar durch union‑find auf Repräsentanten von Termen und Kongruenz‑Propagation bis zum Fixpunkt.

Demonstration

Beginnt man mit a=b und b=c sowie einer binären Funktion f, vereinigt der Algorithmus a,b,c und fügt dann hinzu, dass f(a,d) äquivalent zu f(c,d) für beliebige d ist, und fährt fort, bis keine neuen Kongruenzen entstehen; praktische Varianten bauen und mergen Kongruenzklassen inkrementell und erkennen deduzierbare Gleichheiten effizient.

Fehlanwendung

Den Ground‑Kongruenzabschluss unverändert bei freien Variablen oder interpretierten Theorien zu verwenden führt zu unsicheren oder unvollständigen Ergebnissen; ebenso kann man durch Ersetzung des vollen Theorembeweisers durch Kongruenzabschluss bei Theorie‑Kombinationen notwendige theorie­spezifische Schlüsse übersehen.

Konsequenz

Er liefert ein Entscheidungsverfahren für ground‑äquationale Folgerung in der Theorie uninterpretierter Funktionen und wird als Kern in SMT‑Solve­rern und automatisierten Beweissystemen eingesetzt; effiziente Implementierungen erreichen in typischen Fällen annähernd lineare Laufzeit.

Umkehrung

Statt die kleinste Kongruenz zu berechnen, könnte man eine Überapproximation (z. B. typbasierte Näherung) oder Unterapproximationen von Gleichheiten berechnen; diese Umkehrungen tauschen Korrektheit oder Vollständigkeit gegen Geschwindigkeit oder Einfachheit ein.

Abgrenzung

Standard‑Kongruenzabschluss gilt vor allem für ground‑Terme und uninterpretierte Funktionssymbole; Erweiterungen auf quantifizierte Formeln, interpretierte Theorien (etwa Arithmetik) oder konditionale Gleichungen benötigen zusätzliche Mechanismen wie Quantorinstanziation, Theoriesolver oder Kompletionsverfahren.

Semantische Spannung

Wird häufig mit Unifikation oder Abschlusssystemen der Termumschreibungen verwechselt: Unifikation findet Substitutionen, die Terme gleichmachen, Kompletion erzeugt konfluente Rewritesysteme, während Kongruenzabschluss Gleichheitsklassen von Grundtermen berechnet — verwandte, aber operationell unterschiedliche Aufgaben.

Synthese

Der Kongruenzabschluss‑Algorithmus konstruiert die kleinste unter Funktionsanwendung abgeschlossene Äquivalenzrelation auf Termen durch iteratives Mergen von Klassen und Propagieren von Kongruenzen; er ist der praktische Kern zur Entscheidung ground‑äquationaler Folgerungen in vielen automatisierten Beweissystemen.