\begin{slide}{Aussagenlogische Resolution}

    Formel $(A\vee \neg B\vee \neg C)\wedge(C\vee D)$
    in konjunktiver Normalform

    dargestellt als $\{\{A,\neg B,\neg C\},\{C,D\}\}$

    (Formel $=$ Menge von Klauseln, Klausel $=$ Menge von Literalen,
    Literal $=$ Variable oder negierte Variable)

\bigskip

folgendes Inferenzsystem heißt \emph{Resolution}:
  \begin{itemize}
  \item Axiome: Klauselmenge einer Formel,
  \item Regel: 
    \begin{itemize}
    \item Prämissen: Klauseln $K_1, K_2$
      mit $v\in K_1, \neg v \in K_2$
    \item Konklusion: $(K_1\setminus \{v\})
      \cup (K_2 \setminus \{\neg v\})$
    \end{itemize}
  \end{itemize}

\end{slide}

\begin{slide}{Resolution (Eigenschaften)}

\emph{die Formel (Klauselmenge) ist nicht erfüllbar
  $\iff$  die leere Klausel ist durch Resolution ableitbar.}

Beweispläne:
\begin{itemize}
\item $\Rightarrow$ : 
  Gegeben ist die nicht erfüllbare Formel. Gesucht ist eine Ableitung
  für die leere Klausel. Methode: Induktion nach Anzahl der
  in der Formel vorkommenden Variablen.
\item $\Leftarrow$ : Gegeben ist die Ableitung der leeren Klausel.
  Zu zeigen ist die Nichterfüllbarkeit der Formel.
  Methode: Induktion nach Höhe des Ableitungsbaumes.
\end{itemize}




\end{slide}
