Unifikation--Begriffe

• Signatur $\Sigma$ = $\Sigma_{0}^{}$ $\cup$...$\Sigma_{k}^{}$,
• Term($\Sigma$, V) ist kleinste Menge T mit V $\subseteq$ T und $\forall$0$\le$i$\le$k, f $\in$ $\Sigma_{i}^{}$, t₁ $\in$ T,..., t_i $\in$ T : f (t₁,..., t_i) $\in$ T.
• Substitution: partielle Abbildung $\sigma$ : V$\to$Term($\Sigma$, V), so daß kein v $\in$ dom$\sigma$ in img$\sigma$ vorkommt,
• Substitution $\sigma$ auf Term t anwenden: t$\sigma$
• Produkt von Substitutionen: so definiert, daß t($\sigma_{1}^{}$o$\sigma_{2}^{}$) = (t$\sigma_{1}^{}$)$\sigma_{2}^{}$