Unifikation (Logik)

Unifikation bezeichnet des "gleichsetzen" zweier logischer Variablen.

Beispiel: Es seien zwei Variablen, x und y, gegeben. Sei "x=5". Unifikation wäre jetzt: "y=x".

Dieser Vorgang lässt sich auch formal ausdrücken, der Erkenntnisgewinn ist hier jedoch minimal.

Formalere Definition:

Unifikation ist der Vorgang, wenn zwei Terme durch geeignete Instanziierung (Substitution der Variablen durch Terme) zur Übereinstimmung gebracht werden.

Die Inferenzmaschine des PROLOG-Interpreters nutzt Unifikation.