
\begin{slide}{Übung DPLL(T)}

  \begin{itemize}
  \item 
    ein DPLL(T)-Beispiel für T$=$ 
    Differenzlogik und lineare Ungl. durchrechnen. (evtl. auch autotool)
  \item dabei ggf. T-Entscheidungsverfahren wiederholen.
  \item welche Möglichkeiten bestehen dabei 
    für T-Propagation? T-Lernen?
  \end{itemize}


\end{slide}

\begin{slide}{Übung SMT-LIB}

  \begin{itemize}
  \item einige Beispiele aus SMT-LIB mit Z3 lösen
  \item Beispiele aus SMT-LIB verstehen (warum modelliert die Formel
    das Anwendungsproblem?)
  \item selbst ein Anwendungsproblem in SMT-LIB-Sprache modellieren
  \end{itemize}


\end{slide}
