\newcommand{\QQ}{\mathbb{Q}}

\begin{slide}{Plan}

(für den Rest der Vorlesung)
\begin{itemize}
\item Prädikatenlogik (Syntax, Semantik)
\item existentielle konjunktive Constraints 

in verschiedenen Bereichen, z. B.

% Terme, 
Gleichungen und Ungleichungen auf Zahlen 
% (ganze, rationale, reelle).
$(\ZZ,\QQ,\RR)$
\item beliebige Boolesche Verknüpfungen

  SAT modulo $T$ ($=$ SMT), DPLL($T$)
\item Bit-blasting (SMT $\to$ SAT)
\end{itemize}
\end{slide}
