Kongruenzabschluss

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.