\newcommand{\dom}{\operatorname{dom}}
\newcommand{\img}{\operatorname{img}}
\newcommand{\Term}{\operatorname{Term}}

\begin{slide}{Unifikation---Begriffe}

\begin{itemize}
\item Signatur $\Sigma=\Sigma_0\cup\ldots\Sigma_k$,
\item $\Term(\Sigma,V)$ ist kleinste Menge $T$ mit
  $V\subseteq T$ und $\forall 0\le i\le k, f\in\Sigma_i, t_1\in
  T,\ldots,t_i\in T: f(t_1,\ldots,t_i)\in T$.
\item Substitution: partielle Abbildung $\sigma:V\to\Term(\Sigma,V)$,
  so daß kein $v\in\dom \sigma$ in $\img\sigma$ vorkommt,
\item Substitution $\sigma$ auf Term $t$ anwenden: $t\sigma$
\item Produkt von Substitutionen: so definiert,
  daß $t (\sigma_1 \circ \sigma_2) = (t \sigma_1) \sigma_2$
\end{itemize}

\end{slide}

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

\begin{slide}{Unifikation---Definition}

Unifikationsproblem 
\begin{itemize}
\item Eingabe: Terme $t_1,t_2\in\Term(\Sigma,V)$
\item Ausgabe: eine allgemeinster Unifikator (mgu): 
  Substitution $\sigma$ mit $t_1\sigma = t_2\sigma$.
\end{itemize}

allgemeinst $=$ minimal bzgl. der Prä-Ordnung

$\sigma_1 \le \sigma_2 \iff \exists \tau : \sigma_1 \circ \tau = \sigma_2$

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

\end{slide}

\begin{slide}{Unifikation---Algorithmus}

  $\mgu(s, t)$ nach Fallunterscheidung
  \begin{itemize}
  \item $s$ ist Variable: \dots
  \item $t$ ist Variable: symmetrisch
  \item $s=f(s_1,s_2)$ und $t=g(t_1,t_2)$: \dots
  \end{itemize}

Bemerkungen:
\begin{itemize}
\item korrekt, übersichtlich, aber nicht effizient,
\item es gibt Unif.-Probl. mit exponentiell großer Lösung,
\item eine komprimierte Darstellung davon kann man aber in Polynomialzeit ausrechnen.
\end{itemize}
  
\end{slide}
