
\begin{slide}{Kritische Paare}
Für ein Termersetzungssystem $R$ über $\Sigma$: falls
\begin{itemize} \itemsep 0pt
\item
  $(l_1 \to r_1)$ und $(l_2 \to r_2)$
  sind Regeln in $R$ ohne gemeinsame Variable (ggf. vorher umbenennen!)
\item
  es gibt $p\in\Pos (l_1)$ so daß $l_1[p]$ und $l_2$
  \emph{unifizierbar} sind 

  d. h., es existiert \emph{mgu} $\sigma$ mit $l_1[p]\sigma=l_2\sigma$
\item
  falls $(l_1\to r_1)=(l_2\to r_2)$ (vor Umbenennung),
  dann $p\neq \epsilon$
\item
  dann heißt $(r_1\sigma,(l_1\sigma)[p:=r_2\sigma])$
  \emph{kritisches Paar} von $R$.
\end{itemize}
Ein kritisches Paar $(s,t)$ heißt \emph{zusammenführbar},
falls $\exists u: s\to_R^* u \wedge t\to_R^* u$.


Satz: ein Termersetzungssystem ist genau dann lokal konfluent,
wenn alle kritische Paare zusammenführbar sind.

\end{slide}
