Unifikation

• ein Unifikator von zwei Termen s, t $\in$ Term($\Sigma$, V)

  ist eine Substitution $\sigma$ : V$\to$Term($\Sigma$, V) mit t$\sigma$ = s$\sigma$

• zwei Terme s, t können keinen, einen oder mehrere Unifikatoren haben
• Substitutionen kann man ordnen durch $\sigma_{1}^{}$$\le$$\sigma_{2}^{}$ ($\sigma_{1}^{}$ ist allgemeiner als $\sigma_{2}^{}$) falls $\exists$$\tau$ : $\sigma_{2}^{}$ = $\sigma_{1}^{}$o$\tau$

• Satz: Wenn s, t unifizierbar sind, dann gibt es einen allgemeinsten Unifikator (most general unifier, mgu) $\sigma$ von s und t:

  für jeden Unifikator $\sigma_{2}^{}$ von s und t gilt $\sigma$$\le$$\sigma_{2}^{}$.