\newcommand{\rep}{\operatorname{rep}}

\begin{slide}{Motivation: aussagenlog. Formeln}

\begin{itemize}\itemsep 0pt \parskip 2pt
\item
\emph{kanonisch} repräsentieren

(Def: $\Mod(F)=\Mod(G) \iff \rep(F)=\rep(G)$)
\item
\emph{effizient} vernüpfen ($\rep(F\vee G)=\rep(F) \oplus \rep(G)$)
\end{itemize}

Literatur: 
D. E. Knuth: TAOCP (4A1) 7.1.4; \\
Kroening, Strichman: Decision Procedures, 2.4.
\bigskip
naive Ansätze (Ü: bestimme o.g. Eigenschaften):
\begin{itemize}\itemsep 0pt \parskip 2pt
\item Formel $F$ selbst?
\item Modellmenge $\Mod(F)$ als Menge von Belegungen?
\end{itemize}




\end{slide}
