Ein algorithmischer Mechanismus, der die kleinste Kongruenzrelation berechnet, die eine gegebene Menge von Gleichheiten über Termen enthält, typischerweise durch Verschmelzen von Äquivalenzklassen und Propagieren von Funktionskongruenz, um effiziente Gleichheitsfolgerung, insbesondere für uninterpretiere Funktionen, zu ermöglichen.

Prinzip

Führe Äquivalenzklassen von Termen unter behaupteten Gleichheiten, verschmelze Klassen bei Auftreten von Gleichheiten und sorge dafür, dass wenn f(a1,...,an) und f(b1,...,bn) vorhanden sind und ai ≡ bi für alle i gilt, auch die zusammengesetzten Terme verschmolzen werden; wiederhole dies bis zur Abschlusserreichung.

Demonstration

Gegeben die Gleichheiten a = b und f(a) = c verschmilzt der Abschluss a und b zu einer Klasse, erkennt dann, dass f(a) und f(b) äquivalent sind und verschmilzt deren Klassen, wodurch der Solver weitere Gleichheiten oder Widersprüche effizient folgern kann.

Fehlanwendung

Die Kongruenzschließung naiv auf sehr großen Termgraphen ohne Hash-Consing oder Union-by-Rank anzuwenden kann zu massivem Leistungs- und Speicherzuwachs führen; falsche Behandlung von Funktionsaritäten oder Sorten kann zu unsicheren Verschmelzungen führen.

Konsequenz

Eine korrekte Kongruenzschließung liefert schnelle, kanonische Gleichheitsfolgerung, die in SMT-Engines und Theoremprovern eingesetzt wird und konstante Repräsentantenprüfungen sowie inkrementelle Updates bei Hinzufügung von Gleichheiten ermöglicht.

Umkehrung

Das Gegenteil besteht darin, Gleichheiten nur durch syntaktisches Matching zu behandeln ohne Abschlusspropagation: das bewahrt die Anfangsgleichheiten, verpasst jedoch viele implizite Gleichheiten und hat geringere Schlusskraft.

Abgrenzung

Zielt auf Gleichheitsreasoning für uninterpreted functions in Erster Ordnung und ground-Gleichheiten; behandelt nicht allein interpretierte Theorien (Arithmetik, Arrays) ohne Kombination mit anderen Theorielösern oder Axiomen.

Semantische Spannung

Spannung zwischen Kongruenzschluss und resolution-orientierter Gleichheitsbehandlung: Kongruenzschluss bietet inkrementelle, datenstrukturgetriebene Äquivalenzerhaltung, während Resolution Gleichheiten über Klauselmanipulation behandelt.

Synthese

Kongruenzschluss verschmilzt inkrementell Termäquivalenzklassen und propagiert Funktionskongruenz, um die kleinste Kongruenz zu bilden, die die gegebenen Gleichheiten enthält, und liefert kompaktes, effizientes Gleichheitsreasoning, das sich natürlich in SMT- und Entscheidungsverfahren integriert.