\begin{slide}{Ackermann-Transformation}

\dots von Formel $F$ in \verb|QF_UF| 
nach  Formel $F'$ in \emph{equalitiy logic}
($=$ \verb|QF_UF| mit nur nullstelligen Symbolen)

\begin{itemize}
\item ersetze jeden vorkommenden Teilterm $F_i$ \\
  durch ein neues nullstelliges Symbol $f_i$
\item füge \emph{functional consistency constraints} hinzu:

  für alle $F_i=g(F_{i1},\ldots,F_{ik}), 
  F_j=g(F_{j1},\ldots,F_{jk})$ mit $i\neq j$:

  $(f_{i1}=f_{j1} \wedge \ldots\wedge f_{ik}=f_{jk})
  \rightarrow f_i=f_j$
\end{itemize}

Satz: $F$ erfüllbar $\iff$ $F'$ erfüllbar.



\end{slide}
