Der Prozess, Substitutionen für Variablen zu finden, die zwei syntaktische Ausdrücke (Terme) gemäß der Termalgebra einer Logik identisch machen; liefert eine Substitution, die Variablen auf Terme abbildet, falls eine Lösung existiert.

Prinzip

Ein endliches System von Termgleichungen wird gelöst durch wiederholtes Zerlegen zusammengesetzter Terme, Orientieren von Variablengleichungen, Durchführung eines Occurs-Checks zur Vermeidung zyklischer Substitutionen und Berechnung des allgemeinsten Unifikators, wenn möglich.

Demonstration

Die Unifikation von f(x, a) und f(b, y) liefert die Substitution {x ↦ b, y ↦ a}. In der prädikatenlogischen Resolution wird Unifikation verwendet, um Literale syntaktisch gleich zu machen, bevor die Resolutionsregel angewandt wird.

Fehlanwendung

Das Weglassen des Occurs-Checks und die Akzeptanz von Substitutionen wie x ↦ f(x) erzeugt zyklische oder nicht wohlgegründete Terme; oder die Annahme, Unifikation ergebe stets eine eindeutige Substitution, obwohl in theoretischen oder höherstufigen Kontexten mehrere nicht vergleichbare Unifikatoren oder gar keine existieren können.

Konsequenz

Bei korrekter Anwendung liefert Unifikation die benötigten Substitutionen für automatisches Beweisen, Logikprogrammierung und Typinferenz; der allgemeinste Unifikator erhält maximale Allgemeinheit, was Wiederverwendung und Komposition von Beweisen oder Programmen ermöglicht.

Umkehrung

Die Umkehrung ist die Anti-Unifikation (Generalisation), die statt einer Substitution, die Gleichheit herstellt, die am wenigsten spezialisierte Generalisierung zweier Terme findet; konzeptionell verschiebt die Umkehrung den Fokus vom Lösen von Gleichungen zum Finden gemeinsamer Struktur.

Abgrenzung

Standardmäßige (prädikatenlogische) Unifikation setzt eine syntaktische Termalgebra ohne eingebaute Theorien voraus; sie schließt gleichungstheoretische Unifikation (z. B. modulo Assoziativität oder Kommutativität) sowie höherstufige Unifikation aus, sofern nicht ausdrücklich anders angegeben, da diese unterschiedliche Algorithmen und Entscheidbarkeitseigenschaften haben.

Semantische Spannung

Spannung besteht zwischen Unifikation und Pattern Matching: Matching fixiert eine Seite als Muster zur Instanziierung und liefert eingeschränkte einseitige Substitutionen, während Unifikation symmetrisch ist und allgemeinere Substitutionen zurückgeben kann; eine weitere Spannung liegt zwischen syntaktischer und theoriebasierter Unifikation.

Synthese

Unifikation ist ein algorithmischer Löser für syntaktische Termgleichungen: Durch Zerlegung der Strukturen, Erzwingung von Occurs-Beschränkungen und Berechnung allgemeinster Unifikatoren liefert sie die Substitutionen, die Variableninstanziierung in Inferenz, Programmierung und Typprüfung ermöglichen.