\begin{slide}{Unifikation}

\begin{itemize}
\item
  ein \emph{Unifikator} von zwei Termen $s,t\in\Term(\Sigma,V)$

  ist eine Substitution $\sigma:V\to\Term(\Sigma,V)$  mit $t\sigma=s\sigma$
\item
  zwei Terme $s,t$ können keinen, einen oder mehrere Unifikatoren haben
\item
  Substitutionen kann man ordnen durch $\sigma_1 \le \sigma_2$
  ($\sigma_1$ ist allgemeiner als $\sigma_2$)
  falls $\exists \tau: \sigma_2 = \sigma_1\circ \tau$


\item
  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$.
\end{itemize}

\end{slide}

\newcommand{\mgu}{\operatorname{mgu}}

\begin{slide}{Bestimmung des mgu}

(vergleiche Logische Programmierung)

\begin{itemize}\itemsep 0pt
\item falls $s=t$, dann return identische Abbildung
\item falls $s$ Variable 
\begin{itemize}\itemsep 0pt
\item falls $s$ in $t$ vorkommt, dann fail
\item sonst return $(s \mapsto t)$
\end{itemize}
\item falls $t$ Variable entsprechend
\item falls $s=f(x_1,\ldots)$ und $t=g(y_1,\ldots)$, dann
\begin{itemize}\itemsep 0pt
\item falls $f \neq g$, dann fail, sonst \dots
\item bestimme $\sigma=\mgu(x_1,y_1)$
\item return $\sigma \cup \mgu((x_2\sigma,\ldots),(y_2\sigma,\ldots))$
\end{itemize}
\end{itemize}
Dieser Algorithmus ist korrekt, aber nicht effizient.

\end{slide}
