Unifikation--Definition

Unifikationsproblem

• Eingabe: Terme t₁, t₂ $\in$ Term($\Sigma$, V)
• Ausgabe: eine allgemeinster Unifikator (mgu): Substitution $\sigma$ mit t₁$\sigma$ = t₂$\sigma$.

allgemeinst = minimal bzgl. der Prä-Ordnung

$\sigma_{1}^{}$$\le$$\sigma_{2}^{}$$\iff$$\exists$$\tau$ : $\sigma_{1}^{}$o$\tau$ = $\sigma_{2}^{}$

Satz: jedes Unifikationsproblem ist entweder gar nicht oder bis auf Umbenennung eindeutig lösbar