Unifikation (Logik)

Grundidee und Bedeutung

Unifikation ist eine Methode zur Vereinheitlichung prädikatenlogischer Ausdrücke. Dabei werden Variablen durch geeignete Terme ersetzt, sodass die entstehenden Ausdrücke gleich sind. Die Methode ist wichtig für die Computerlogik und die Computerlinguistik. In Prolog verwendet die Inferenzmaschine Unifikation; außerdem beruhen Unifikationsgrammatiken und viele Verfahren des Theorembeweisens auf diesem Konzept.

Die Grundlage der Unifikation ist die Substitution. In der Prädikatenlogik bedeutet eine Substitution σ, dass innerhalb eines gegebenen Ausdrucks eine Variable durch einen Term ersetzt wird. Die ersetzte Variable darf in diesem Term nicht selbst vorkommen. Die Variable wird dadurch instanziiert, also auf einen bestimmten Term festgelegt.

Gegeben sei eine Menge von Ausdrücken {A₁, A₂, …, Aₙ}. Eine Substitution σ heißt Unifikator dieser Ausdrucksmenge, wenn nach ihrer Anwendung alle Ausdrücke äquivalent beziehungsweise gleich sind: σ(A₁) ≡ σ(A₂) ≡ ⋯ ≡ σ(Aₙ). Die Anwendung eines Unifikators auf eine Ausdrucksmenge heißt Unifikation. Nicht jede Menge von Ausdrücken kann unifiziert werden.

Beispiel einer Unifikation

Gegeben sind die Ausdrücke A₁ = (X, Y, f(b)) und A₂ = (a, b, Z).

Dabei stehen Großbuchstaben für Variablen und Kleinbuchstaben für atomare Ausdrücke. Die Ausdrücke werden gleich, wenn X durch a, Y durch b und Z durch f(b) ersetzt wird. Der Unifikator lautet daher: σ = {X ↦ a, Y ↦ b, Z ↦ f(b)}.

Nach der Substitution erhält man: σ(A₁) = (a, b, f(b)) σ(A₂) = (a, b, f(b)).

Beide Ausdrücke sind damit identisch und erfolgreich unifiziert.

Kleinster gemeinsamer Unifikator

Für eine Ausdrucksmenge gibt es gewöhnlich mehrere Unifikatoren. Ein Unifikator μ heißt kleinster gemeinsamer Unifikator oder allgemeinster Unifikator, wenn sich jeder andere Unifikator σ aus μ durch eine weitere Substitution τ gewinnen lässt. Formal gilt: σ = τ ∘ μ.

Dabei bedeutet τ ∘ μ, dass die Substitutionen hintereinander ausgeführt werden. Der allgemeinste Unifikator enthält somit nur die notwendigen Vereinheitlichungen; speziellere Unifikatoren entstehen durch zusätzliche Ersetzungen. Ein kleinster gemeinsamer Unifikator ist nicht notwendigerweise eindeutig.

Für unifizierbare Ausdrücke kann der Unifikationsalgorithmus von Robinson einen kleinsten gemeinsamen Unifikator bestimmen. Der Algorithmus geht schrittweise von den Unterschieden der Ausdrücke aus und ergänzt die erforderlichen Substitutionen.

Unifikationsalgorithmus

Der Algorithmus erhält als Eingabe eine Menge von Ausdrücken A und gibt als Ergebnis den allgemeinsten Unifikator sub aus.

Zu Beginn wird sub auf die leere Substitution gesetzt: sub := ∅.

Solange die durch sub veränderte Ausdrucksmenge sub(A) mehr als einen Ausdruck enthält, werden die Ausdrücke von links nach rechts durchsucht. Gesucht wird die erste Position, an der sich zwei Ausdrücke in einem Zeichen unterscheiden.

• Sind beide unterschiedlichen Zeichen keine Variablen, sind die Ausdrücke nicht unifizierbar. Der Algorithmus gibt „nicht unifizierbar“ aus und endet.
• Ist eines der Zeichen eine Variable, wird diese Variable X genannt. Der Term, der an derselben Stelle im anderen Ausdruck beginnt, wird mit t bezeichnet; t kann ebenfalls eine Variable sein.
• Kommt X in t vor, sind die Ausdrücke ebenfalls nicht unifizierbar. Der Algorithmus gibt „nicht unifizierbar“ aus und endet. Dadurch wird verhindert, dass eine Variable durch einen Term ersetzt wird, der sie selbst enthält.
• Kommt X nicht in t vor, wird die Substitution um [X/t] ergänzt: sub := sub[X/t]. Die bisherige Substitution und [X/t] werden hintereinander ausgeführt.

Dieser Vorgang wird wiederholt, bis alle Ausdrücke in sub(A) gleich sind. Dann gibt der Algorithmus sub als allgemeinsten Unifikator aus.