\begin{slide}{Nelson-Oppen (I)}

(Wdhlg) Formel/Ausdruck

purification (Reinigung):

\begin{itemize}
\item durch Einführen neuer Variablen:
\item alle atomaren Formeln
  enthalten nur Ausdrücke \emph{einer} Theorie
\end{itemize}

Beispiel:
\begin{itemize}
\item vorher: $\phi:=x_1 \le f(x_1)$
\item nachher: $\phi':= x_1 \le a \wedge a=f(x_1)$
\end{itemize}

im Allg. $\phi \iff \exists a,\ldots: \phi'$

d. h. $\phi$ erfüllbar $\iff$ $\phi'$ erfüllbar.

\end{slide}
