Der algorithmische Prozess, eine Substitution (Abbildung von Variablen auf Terme) zu finden, die zwei symbolische Ausdrücke bis auf syntaktische Gleichheit (oder Gleichheit modulo einer Theorie) identisch macht; zentral für automatisches Schließen, Typinferenz und Logikprogrammierung.

Prinzip

Suche nach einem allgemeinsten Unifikator (mgu), der die Matching‑Gleichungen zwischen entsprechenden Untertermen löst, ohne unnötige Instantiierungen einzuführen; die Occur‑Check verhindert zyklische Substitutionen, und Varianten umfassen syntaktische Erstordnungsunifikation, E‑Unifikation (modulo äquationaler Theorien) und höherordentliche Unifikation mit sehr unterschiedlichen Entscheidbarkeits‑ und Komplexitätsprofilen.

Demonstration

Erstordnungsbeispiel: Unifiziere f(x,a) und f(b,y) — der mgu ist {x↦b, y↦a}. Occur‑Check‑Beispiel: Die Unifikation von x und f(x) schlägt fehl, weil jede Lösung zyklisch wäre (bei Erstordnungsunifikation wird dies durch den Occur‑Check abgelehnt). Höherordentliches Beispiel: Unifikation im λ‑Kalkül ist im Allgemeinen unentscheidbar und erfordert andere Algorithmen (z. B. Huets semi‑entscheider Verfahren) oder Einschränkungen zur Entscheidbarkeit.

Fehlanwendung

Das Weglassen des Occur‑Checks in Implementierungen führt zu unsauberen Substitutionen, die unendliche Terme und falsche Ergebnisse zulassen. Das Anwenden von Erstordnungsunifikationsalgorithmen auf Probleme mit assoziativ/kommutativen Operatoren oder höherordentlichen Bindern ohne geeignete E‑Unifikations‑ bzw. höherordentliche Behandlung führt zu falscher oder unvollständiger Unifikation.

Konsequenz

Unifikation liefert die Substitutionen, die für die Resolution in der Erstordnungsbeweiser, für Typinferenz in Programmiersprachen und für Matching in Rewriting‑Systemen benötigt werden; wenn mgus existieren, ermöglichen sie allgemeine, wiederverwendbare Lösungen, während die Unentscheidbarkeit oder Intractability in ausdrucksstärkeren Einstellungen das automatische Schließen einschränkt und Heuristiken oder beschränkte Fragmente erforderlich macht.

Umkehrung

Matching (einseitige Unifikation) beschränkt Variablen auf einen Ausdruck und ist rechnerisch einfacher; Anti‑Unifikation (Generalisierung) berechnet die am wenigsten allgemeinen Generalisatoren statt der allgemeinsten Unifikatoren. Die Umkehr der Unifikation verschiebt konzeptionell vom Lösen von Gleichungen zum Finden schematischer Abstraktionen.

Abgrenzung

Erstordnungs‑syntaktische Unifikation ist entscheidbar und besitzt allgemeinste Unifikatoren, wenn lösbar; Unifikation modulo Theorien (AC, assoziativ‑kommutativ, etc.) oder höherordentliche Unifikation kann unentscheidbar oder viel komplexer sein. Exakte Eigenschaften hängen von der betrachteten Logik und Theorie ab.

Semantische Spannung

Spannung zwischen syntaktischer Unifikation (reine Termstruktur) und semantischer Unifikation (modulo Theorien) beeinflusst sowohl Vollständigkeit als auch Performance; es ergeben sich Trade‑offs zwischen reichhaltigerem äquationalen Schließen und algorithmischer Handhabbarkeit.

Synthese

Unifikation ist der Prozess des Berechnens von Substitutionen, die Terme unter einer gewählten Gleichheitsauffassung gleichmachen; als Kernoperation im automatischen Schließen und in Typensystemen balanciert sie das Streben nach allgemeinsten, wiederverwendbaren Lösungen gegen Beschränkungen durch Occurence‑Checks, äquationale Theorien und höherordentliche Merkmale, die Entscheidbarkeit und Komplexität verändern.