## [Unifikation](/de/node/59919) Definition 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 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 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 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 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 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 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 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 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.