Unifikation (Logik)

Unifikation ist eine Methode zur Vereinheitlichung prädikatenlogischer Ausdrücke. Zwei Ausdrücke werden unifiziert, indem ihre Variablen so durch geeignete Terme ersetzt werden, dass die resultierenden Ausdrücke gleich sind. Die Unifikation hat insbesondere in der Computerlogik und Computerlinguistik eine größere Bedeutung erlangt. So nutzt etwa die Inferenzmaschine des Prolog-Interpreters Unifikation. In der Computerlinguistik gibt es sogenannte Unifikationsgrammatiken, die sich auf dieses Konzept stützen. Auch beim Theorembeweisen spielt Unifikation eine große Rolle.

Als Basisoperation liegt der Unifikation die Substitution zu Grunde. Im Rahmen der Prädikatenlogik bedeutet eine Substitution σ innerhalb eines gegebenen Ausdrucks die Ersetzung einer Variablen durch einen Term, in dem diese Variable nicht vorkommen darf. Die Variable wird gewissermaßen durch den Term „instanziiert“.

Wird eine Menge von Ausdrücken ${\displaystyle \{A_{1},A_{2},\ldots ,A_{n}\}}$ durch eine Substitution σ zu einem äquivalenten Ausdruck substituiert, d. h. ${\displaystyle \sigma (A_{1})\equiv \sigma (A_{2})\equiv \cdots \equiv \sigma (A_{n})}$, so bezeichnet man σ als Unifikator dieser Ausdrucksmenge. Die Anwendung eines Unifikators auf diese Menge bezeichnet man als Unifikation. Nicht alle Ausdrucksmengen können unifiziert werden.