\begin{slide}{(Dis)Equality Constraints (Bsp, Def)}
%
\begin{eqnarray*}
&& (a_0=b_0 \wedge b_0=a_1 \vee a_0=c_0 \wedge c_0=a_1) \wedge \ldots\\
& \wedge& (a_n=b_n \wedge b_n=a_{n+1} \vee a_n=c_n \wedge c_n=a_{n+1}) \\
& \wedge& a_{n+1} \neq a_0
\end{eqnarray*}
%
(Quelle: Strichman, Rozanov, SMT Workshop 2007,
\begin{tiny}
\url{http://www.lsi.upc.edu/~oliveras/espai/smtSlides/ofer.ppt},
\url{http://smtexec.org/exec/smtlib-portal-benchmarks.php?download&inline&b=QF_UF/eq_diamond/Feq_diamond10.smt2}
\end{tiny}


Formel $\exists x_1,\ldots,x_n : M$ 
mit $M$ in negationstechnischer Normalform über
Signatur: 
\begin{itemize} \itemsep 2pt
\item Prädikatsymbole $=$ und $\neq$, keine Funktionssymbole
\end{itemize}

\end{slide}

