\begin{slide}{Beweise für Nichterfüllbarkeit}

  \begin{itemize}
  \item 
bisher: Interesse an erfüllender Belegung 
$m\in\Mod(F)$ ($=$ Lösung einer Anwendungsaufgabe)

\item

jetzt: Interesse an $\Mod(F)=\emptyset$.

Anwendungen: Schaltkreis $C$ erfüllt
Spezifikation $S$ $\iff$ 
$\Mod(C(x) \neq S(x)) = \emptyset$.
\end{itemize}

Solver rechnet lange, evtl. Hardwarefehler usw.
\begin{itemize}
\item
  $m\in\Mod(F)$ kann man leicht prüfen

  (unabhängig von der Herleitung)
\item
  wie prüft man $\Mod(F)=\emptyset$?

  (wie sieht ein \emph{Zertifikat} dafür aus?)
\end{itemize}


\end{slide}


