\defineUnit{aussagenlogiksyntax}{%
\begin{frame}[c]
    \frametitle{Syntax der Aussagenlogik}
    \setbeamercovered{dynamic}

    \begin{definition}[Syntax der Aussagenlogik]
        Aussagenlogische \structure{Formeln} bestehen aus Konstanten, Variablen und Operatoren. Die Menge \structure{$\mathcal{F}$} aller Formeln ist induktiv definiert.
        \begin{itemize}
            \item $\false = 0 = \bot \in \mathcal{F},\quad \true = 1 = \top \in \mathcal{F}$\hfill(\alert{Konstanten})
            \item $V = \left\{ a, b, c,\ldots \right\} \subseteq \mathcal{F}$\hfill(\alert{Variablen})\\
            \medskip
            \item Ist $A \in \mathcal{F}$ eine aussagenlogische Formel, dann auch
                \begin{align}
                    \neg A &\in \mathcal{F}\tag{\alert{Negation}}\\
            \intertext{\item Sind $A, B \in \mathcal{F}$ aussagenlogische Formeln, dann auch}
                    (A \wedge B)&\in \mathcal{F}\tag{\alert{Konjunktion}}\\
                    (A \vee B)&\in \mathcal{F}\tag{\alert{Disjunktion}}\\
                    (A \rightarrow B)&\in \mathcal{F}\tag{\alert{Implikation}}
                \end{align}
        \end{itemize}
        Alle Formeln lassen sich so konstruieren.
    \end{definition}
\end{frame}

\begin{frame}
    \frametitle{Operatorenbindung}
    \setbeamercovered{dynamic}

    \begin{definition}[Bindungsregeln]
        Die \structure{Bindungsstärke} der Operatoren in absteigender Reihenfolge ist
        \[ \neg \quad \wedge \quad \vee \quad \rightarrow \quad \leftrightarrow \]
        Die Implikation ist \structure{rechtsassoziativ}
        \[ a \rightarrow b \rightarrow c \rightarrow d\text{\quad steht für\quad} \left( a \rightarrow \left( b \rightarrow \left( c \rightarrow d \right) \right) \right) \]
    \end{definition}
    \begin{itemize}
        \item Üblicherweise klammert man $\wedge$ und $\vee$
            \[ (a \wedge b) \vee c \text{\quad statt\quad} a \wedge b \vee c \]
    \end{itemize}
    \begin{example}[]
        \begin{itemize}
            \item $\neg a \wedge b$\quad steht für \quad$ \left( \left( \neg a \right) \wedge b \right)$
            \item $a \wedge b \rightarrow c \vee \neg d$\quad steht für \quad$((a \wedge b) \rightarrow (c \vee \left( \neg d \right)))$
        \end{itemize}
    \end{example}
\end{frame}

\begin{frame}
    \frametitle{Syntaxbaum}
    \setbeamercovered{dynamic}

    \begin{block}{Syntaxbaum}
        \structure{Syntaxbäume} visualisieren in welcher Reihenfolge die Regeln zur induktiven Definition angewandt werden müssen, um eine Formel zu erzeugen.
    \end{block}
    \begin{example}[]
        Sei $F \defeq a \wedge b \rightarrow c \vee \neg d$ dann ist der dazu passende Syntaxbaum
        \centering
        \begin{tikzpicture}[grow=down, level distance = 33]
            \tikzstyle{every node} = []
            \tikzstyle{op} = [pretty]
            \tikzstyle{var} = [pretty, rectangle]
            \tikzstyle{edge from parent} = [edge]

            \tikzstyle{level 1} = [sibling distance = 80]
            \tikzstyle{level 2} = [sibling distance = 40]
            \node[op] {$\rightarrow$}
                child {
                    node[op] {$\wedge$}
                    edge from parent
                    child {
                        node[var] {$a$}
                        edge from parent
                    }
                    child {
                        node[var] {$b$}
                        edge from parent
                    }
                }
                child {
                    node[op] {$\vee$}
                    edge from parent
                    child {
                        node[var] {$c$}
                        edge from parent
                    }
                    child {
                        node[op] {$\neg$}
                        edge from parent
                        child {
                            node[var] {$d$}
                            edge from parent
                        }
                    }
                };
        \end{tikzpicture}
    \end{example}
\end{frame}
}

\defineUnit{aussagenlogiksemantik}{%
\begin{frame}
    \frametitle{Belegung}
    \setbeamercovered{dynamic}

    \begin{definition}[Belegung]
        Eine passende \structure{Belegung} $\beta$ zu einer Formel $F$ ordnet jeder Variable in $V$ einen Wahrheitswert aus $\left\{ 0, 1 \right\}$ zu. Es ist
        \[ \beta : V \to \left\{ 0, 1 \right\} \]
    \end{definition}
    \begin{itemize}
        \item Belegungen formalisieren Einsetzen
        \item Für $n$ Variablen existieren $2^n$ Belegungen
    \end{itemize}
    \begin{example}[]
        Sei $F \defeq \neg \left( a \wedge b \right)$ mit $V = \left\{ a, b \right\}$ und
        \begin{align}
            \beta : \left\{ a, b \right\} &\to \left\{ 0, 1 \right\}\\
            a &\mapsto 1\\
            b &\mapsto 0
        \end{align}
        Dann ist $\beta$ eine zu $F$ passende \structure{Belegung}.
    \end{example}
\end{frame}

\begin{frame}
    \frametitle{Semantik der Aussagenlogik}
    \setbeamercovered{dynamic}

    \begin{definition}[Semantik einer Formel]
        Die \structure{Semantik} $[F]$ einer aussagenlogischen Formel $F$ ist eine Funktion, die jeder passenden Belegung $\beta$ einen Wahrheitswert zuordnet.\\
        Sei $\mathcal{B} = \left\{ \beta_0, \beta_1, \ldots \right\}$ die Menge aller Belegungen zu $F$. Dann ist
        \[[F] : \mathcal{B} \to \left\{ 0, 1 \right\}\]
    \end{definition}
    \begin{itemize}
        \item Die Semantik löst eingesetzte Formeln auf
        \item Wird anhand der induktiven Syntax definiert
        \item Es gibt \alert{syntaktisch verschiedene} Formeln gleicher \structure{Semantik}
    \end{itemize}
    \begin{example}[]
        Sei $F \defeq \left( G \rightarrow H \right)$ mit $G, H$ Formeln. Dann ist
        \[ [F](\beta) = \begin{cases}
                0 & \text{falls } [G](\beta) = 1 \text{ und } [H](\beta) = 0 \\
                1 & \text{sonst}
                \end{cases}\]
    \end{example}
\end{frame}

\begin{frame}
    \frametitle{Wahrheitstabelle}
    \setbeamercovered{dynamic}

    \begin{block}{Wahrheitstabelle}
        Die Semantik einer Formel kann mit Hilfe einer \structure{Wahrheitstabelle} visualisiert werden. Die Tabelle gibt den Wahrheitswert der Formel für jede mögliche Belegung an.
    \end{block}
    \begin{example}[]
        Sei $F \defeq a \vee b \rightarrow \neg c \wedge b$. Die zu $[F]$ gehörige Wahrheitstabelle ist
        \begin{center}
            \begin{tabu} to .5\textwidth {cccX|[1.2pt]Xccccc}
                a & b & c & & & $a \vee b$ & $\rightarrow$ & $\neg c$ & $\wedge$ & $b$ \\ \tabucline[1.2pt]{-}
                0 & 0 & 0 & & & \onslide<2->{0} & \onslide<3->{\structure{1}} & \onslide<2->{1} & \onslide<2->{0} & \\
                0 & 0 & 1 & & & \onslide<2->{0} & \onslide<3->{\structure{1}} & \onslide<2->{0} & \onslide<2->{0} & \\
                0 & 1 & 0 & & & \onslide<2->{1} & \onslide<3->{\structure{1}} & \onslide<2->{1} & \onslide<2->{1} & \\
                0 & 1 & 1 & & & \onslide<2->{1} & \onslide<3->{\structure{0}} & \onslide<2->{0} & \onslide<2->{0} & \\
                1 & 0 & 0 & & & \onslide<2->{1} & \onslide<3->{\structure{0}} & \onslide<2->{1} & \onslide<2->{0} & \\
                1 & 0 & 1 & & & \onslide<2->{1} & \onslide<3->{\structure{0}} & \onslide<2->{0} & \onslide<2->{0} & \\
                1 & 1 & 0 & & & \onslide<2->{1} & \onslide<3->{\structure{1}} & \onslide<2->{1} & \onslide<2->{1} & \\
                1 & 1 & 1 & & & \onslide<2->{1} & \onslide<3->{\structure{0}} & \onslide<2->{0} & \onslide<2->{0} & \\
            \end{tabu}
        \end{center}
    \end{example}
\end{frame}

\begin{frame}
    \frametitle{Äquivalente Formeln}
    \setbeamercovered{dynamic}

    \begin{definition}[Äquivalente Formeln]
        Man nennt zwei Formeln \structure{äquivalent}, wenn sie dieselbe Semantik besitzen.\\
        Seien $F, G$ Formeln mit Belegungen $\mathcal{B} = \mathcal{B}_F = \mathcal{B}_G$. $F$ und $G$ sind äquivalent wenn
        \[ \forall \beta \in \mathcal{B}. [F](\beta) = [G](\beta) \]
        Man schreibt \structure{$F \equiv G$} oder \structure{$F \leftrightarrow G$}.
    \end{definition}

    \begin{example}[]
        Für $F \defeq a \rightarrow b$ und $G \defeq \neg a \vee b$ gilt $F \equiv G$.
        \begin{center}
            \begin{tabu} to .4\textwidth {cc|[1.2pt]XcX||Xccc}
                a & b & & $a \rightarrow b$ & & & $\neg a$ & $\vee$ & $b$ \\ \tabucline[1.2pt]{-}
                0 & 0 & & \structure{1} & & & 1 & \structure{1} \\
                0 & 1 & & \structure{1} & & & 1 & \structure{1} \\
                1 & 0 & & \structure{0} & & & 0 & \structure{0} \\
                1 & 1 & & \structure{1} & & & 0 & \structure{1} \\
            \end{tabu}
        \end{center}
    \end{example}
\end{frame}

\begin{frame}
    \frametitle{Eigenschaften von Formeln}
    \setbeamercovered{dynamic}

    \begin{block}{Eigenschaften aussagenlogischer Formeln}
        Sei $F$ eine aussagenlogische Formel mit Variablen $V$ und der Menge der passenden Belegungen $\mathcal{B}$. Man nennt F
        \begin{description}[\quad unerfüllbar]
            \item[erfüllbar] $\exists \beta \in \mathcal{B}. [F](\beta) = 1$\hfill($F$ kann wahr sein)
            \item[unerfüllbar] $\forall \beta \in \mathcal{B}. [F](\beta) = 0$\hfill($F$ ist nie wahr)
            \item[gültig] $\forall \beta \in \mathcal{B}. [F](\beta) = 1$\hfill($F$ ist immer wahr)
        \end{description}
    \end{block}
    \begin{itemize}
        \item Eine unerfüllbare Formel nennt man \structure{Widerspruch}
        \item Eine gültige Formel nennt man \structure{Tautologie}
    \end{itemize}

\end{frame}
}

\defineUnit{aussagenlogikaequivalenzen}{%
{
    \newcommand{\spc}{\hfill}
    \newcommand{\F}{F}
    \newcommand{\G}{G}
    \newcommand{\K}{H}

    \begin{frame}
        \frametitle{Äquivalenzregeln}
        \setbeamercovered{dynamic}

        \begin{description}[Triviale Kontradiktion\quad]
            \item[Identität] $\F \wedge \true \equiv \F \spc \F \vee \false \equiv \F$
            \item[Dominanz] $\F \vee \true \equiv \true \spc \F \wedge \false \equiv \false$
            \item[Idempotenz] $\F \vee \F \equiv \F \spc \F \wedge \F \equiv \F$
            \item[Doppelte Negation] $\neg \neg \F \equiv \F$
            \item[Triviale Tautologie] $\F \vee \neg \F \equiv \true$
            \item[Triviale Kontradiktion] $\F \wedge \neg \F \equiv \false$
                \bigskip
            \item[Kommutativität] $\F \vee \G \equiv \G \vee \F$\\
                $\F \wedge \G \equiv \G \wedge \F$
            \item[Assoziativität] $(\F \vee \G) \vee \K \equiv \F \vee (\G \vee \K)$\\
                $(\F \wedge \G) \wedge \K \equiv \F \wedge (\G \wedge \K)$
            \item[Distributivität] $\F \vee (\G \wedge \K) \equiv (\F \vee \G) \wedge (\F \vee \K)$\\
                $\F \wedge (\G \vee \K) \equiv (\F \wedge \G) \vee (\F \wedge \K)$
            \item[De Morgan] $\neg(\F \wedge \G) \equiv \neg \F \vee \neg \G$\\
                $\neg(\F \vee \G) \equiv \neg\F \wedge \neg\G$
                \bigskip
            \item[Implikation] $\F \rightarrow \G \equiv \neg \F \vee \G$
            \item[Bikonditional] $\F \leftrightarrow \G \equiv \neg(\F \otimes \G) \left[ \equiv (\F \rightarrow \G) \wedge (\G \rightarrow \F) \right]$
        \end{description}
    \end{frame}

    %\begin{frame}
        %\frametitle{Äquivalenzregeln}
        %\setbeamercovered{dynamic}

        %\vspace{-2em}
        %\begin{align}
            %\F \wedge \true &\equiv \F \spc \F \vee \false \equiv \F \tag{\structure{Identität}}\\
            %\F \vee \true &\equiv \true \spc \F \wedge \false \equiv \false \tag{\structure{Dominanz}}\\
            %\F \vee \F &\equiv \F \spc \F \wedge \F \equiv \F \tag{\structure{Idempotenz}}\\
            %\neg \neg \F &\equiv \F \tag{\structure{Doppelte Negation}}\\
            %\F \vee \neg \F &\equiv \true \tag{\structure{Triviale Tautologie}}\\
            %\F \wedge \neg \F &\equiv \false \tag{\structure{Triviale Kontradiktion}}\\
                %\bigskip
            %\F \vee \G &\equiv \G \vee \F \tag{\structure{Kommutativität}}\\
                %\F \wedge \G &\equiv \G \wedge \F\\
            %(\F \vee \G) \vee \K &\equiv \F \vee (\G \vee \K) \tag{\structure{Assoziativität}}\\
                %(\F \wedge \G) \wedge \K &\equiv \F \wedge (\G \wedge \K)\\
            %\F \vee (\G \wedge \K) &\equiv (\F \vee \G) \wedge (\F \vee \K) \tag{\structure{Distributivität}}\\
                %\F \wedge (\G \vee \K) &\equiv (\F \wedge \G) \vee (\F \wedge \K)\\
            %\neg(\F \wedge \G) &\equiv \neg \F \vee \neg \G \tag{\structure{De Morgan}}\\
                %\neg(\F \vee \G) &\equiv \neg\F \wedge \neg\G\\
                %\bigskip
            %\F \rightarrow \G &\equiv \neg \F \vee \G \tag{\structure{Implikation}}\\
            %\F \leftrightarrow \G &\equiv (\F \rightarrow \G) \wedge (\G \rightarrow \F) \tag{\structure{Bikonditional}}\\
        %\end{align}
    %\end{frame}
}
}

\defineUnit{aussagenlogiknormalformen}{%
\begin{frame}[c]
    \frametitle{Literale und Klauseln}
    \setbeamercovered{dynamic}

    \begin{definition}[Literal]
        Ein \structure{Literal} ist eine Variable $v \in V$ oder die Negation $\neg v$ einer Variable.
    \end{definition}

    \begin{definition}[Klausel]
        Eine \structure{Klausel} verknüpft mehrere Literale mit einem assoziativen Operator.
    \end{definition}

    \vfill

    \begin{example}[]
        Seien $a, \neg b, c$ Literale. Dann sind
        \begin{itemize}
            \item $a \wedge \neg b \wedge c$
            \item $a \vee \neg b \vee c$
        \end{itemize}
        Klauseln.
    \end{example}
\end{frame}

{
    \newcommand{\klausel}[2]{\underbracket{(##2)}_{\text{##1-Klausel}}}
    \begin{frame}
        \frametitle{DNF}
        \setbeamercovered{dynamic}

        \begin{definition}[Disjunktive Normalform]
            Eine \structure{DNF-Klausel} ist eine Konjunktion von Literalen $L_i$.\\
            Eine Formel $F$, ist in \structure{Disjunktiver Normalform}, wenn sie eine Disjunktion von DNF-Klauseln ist.
            \[ F \defeq \bigvee \bigwedge_i L_i \]
        \end{definition}
        \begin{itemize}
            \item Ausnahme: $\false$ ist auch in DNF
        \end{itemize}

        \begin{example}[]
            $F$ ist in DNF.
            \[ F \defeq \klausel{DNF}{a \structure{\wedge} b \structure{\wedge} \neg c} \alert{\vee} \klausel{DNF}{\neg b \structure{\wedge} c} \alert{\vee} \klausel{DNF}{\neg a \structure{\wedge} b \structure{\wedge} \neg c} \]
        \end{example}
    \end{frame}

    \begin{frame}
        \frametitle{KNF}
        \setbeamercovered{dynamic}

        \begin{definition}[Konjunktive Normalform]
            Eine \structure{KNF-Klausel} ist eine Disjunktion von Literalen $L_i$.\\
            Eine Formel $F$, ist in \structure{Konjunktiver Normalform}, wenn sie eine Konjunktion von KNF-Klauseln ist.
            \[ F \defeq \bigwedge \bigvee_i L_i \]
        \end{definition}
        \begin{itemize}
            \item Ausnahme: $\true$ ist auch in KNF
        \end{itemize}

        \begin{example}[]
            $F$ ist in KNF.
            \[ F \defeq \klausel{KNF}{\neg a \alert{\vee} b} \structure{\wedge} \klausel{KNF}{\neg b \alert{\vee} c} \structure{\wedge} \klausel{KNF}{a \alert{\vee} b \alert{\vee} \neg c} \]
        \end{example}
    \end{frame}
}

\begin{frame}
    \frametitle{Konstruktion der NF}
    \setbeamercovered{dynamic}

    \begin{itemize}
        \item \structure{Jede} nicht-triviale Formel ist in DNF und KNF umwandelbar
        \item Durch Äquivalenzumformungen berechenbar (exponentiell groß!)
        \item Oder: Konstruktion mit Wahrheitstabellen
    \end{itemize}

    \vfill

    \begin{block}{Normalformen aus Wahrheitstabellen}
        Gegeben eine Formel $F$ und ihre Wahrheitstabelle
        \begin{itemize}
            \item DNF
                \begin{enumerate}
                    \item Betrachte Zeilen mit Eintrag \structure{$1$}
                    \item Bilde \structure{Konjunktion} aus der \structure{Belegung}
                    \item Bilde \structure{Disjunktion} aller erhaltenen Klauseln
                \end{enumerate}
                \bigskip
            \item KNF
                \begin{enumerate}
                    \item Betrachte Zeilen mit Eintrag \alert{$0$}
                    \item Bilde \alert{Disjunktion} aus der \alert{Negation} der Belegung
                    \item Bilde \alert{Konjunktion} aller erhaltenen Klauseln
                \end{enumerate}
        \end{itemize}
    \end{block}
\end{frame}

{
    \newcommand{\klausel}[4]{(##2 a ##1 ##3 b ##1 ##4 c)}
    \begin{frame}
        \frametitle{Konstruktion der NF}
        \setbeamercovered{dynamic}

        \begin{example}[]
            Gegeben eine Formel $F$ mit folgender Semantik
            \begin{center}
                \begin{tabu} to .4\textwidth {ccc|[1.2pt]c}
                    a & b & c & $F$ \\ \tabucline[1.2pt]{-}
                    0 & 0 & 0 & 0 \\
                    0 & 0 & 1 & 0 \\
                    0 & 1 & 0 & 0 \\
                    0 & 1 & 1 & 1 \\
                    1 & 0 & 0 & 1 \\
                    1 & 0 & 1 & 1 \\
                    1 & 1 & 0 & 1 \\
                    1 & 1 & 1 & 0
                \end{tabu}
            \end{center}
            $F$ dargestellt in
            \begin{itemize}
                \item DNF $\hfill\klausel{\wedge}{\neg}{}{} \vee (a \wedge \neg b) \vee \klausel{\wedge}{}{}{\neg}\hfill$
                    \medskip
                \item KNF $\hfill(a \vee b) \wedge \klausel{\vee}{\neg}{}{\neg} \wedge \klausel{\vee}{\neg}{\neg}{\neg}\hfill$
            \end{itemize}
        \end{example}
    \end{frame}

    \begin{frame}
        \frametitle{Mengendarstellung der KNF}
        \setbeamercovered{dynamic}

        \begin{block}{Mengendarstellung der KNF}
            Eine Formel $F = \bigwedge \bigvee L_i$ in \structure{KNF} kann in einer \structure{Mengendarstellung} repräsentiert werden.
            \begin{itemize}
                \item Klauseln werden durch Mengen von Literalen dargestellt
                    \[\left\{ a, \neg b, c \right\} \text{ steht für } (a \vee \neg b \vee c)\]
                \item KNF-Formeln sind Mengen von Klauseln
                    \[ \left\{ \left\{ \neg a \right\}, \left\{ a, \neg b, c \right\} \right\} \text{ steht für } \neg a \wedge (a \vee \neg b \vee c) \]
                \item $\emptyset$ steht für $\true$, $\left\{ \emptyset \right\}$ für $\false$
            \end{itemize}
        \end{block}
        \begin{example}[]
            Gegeben $F \defeq (a \vee b) \wedge \klausel{\vee}{\neg}{}{\neg} \wedge \klausel{\vee}{\neg}{\neg}{\neg}$ in KNF.
            \[ \left\{ \left\{ a, b \right\}, \left\{ \neg a, b, \neg c \right\}, \left\{ \neg a, \neg b, \neg c \right\} \right\}\]
        \end{example}
    \end{frame}
}
}

\defineUnit{DPLL}{%
\begin{frame}
    \frametitle{KNF aus Syntaxbaum}
    \setbeamercovered{dynamic}

    \begin{block}{Idee}
        Erzeuge die KNF aus dem Syntaxbaum
        \begin{enumerate}
            \item<1-> Weise jedem \structure{inneren Knoten} eine Variable zu
            \item<1,3-> Variablen sind \structure{abhängig} von ihren Kindern
            \item<1,4-> Berechne \structure{kleine} KNFs und führe diese \structure{zusammen}
        \end{enumerate}
    \end{block}
    \begin{columns}[T]
        \begin{column}{.7\textwidth}
            % FIXME: onlys around A_\vee needed for "correct" fadein
            \begin{align}
                (x \wedge y) \vee z
                \uncover<3->{\equiv &\hphantom{{}\wedge {}}\only<3->{A_\vee}\\
                    &\structure{\wedge (A_\vee \leftrightarrow A_\wedge \vee z)}\\
                    &\alert{\wedge (A_\wedge \leftrightarrow x \wedge y)}\\}
                \uncover<4->{\equiv &\hphantom{{}\wedge {}}\only<4->{A_\vee}\\
                    &\structure{\wedge (A_\vee \vee \neg A_\wedge) \wedge (A_\vee \vee \neg z)}\\
                    &\qquad\structure{\wedge (\neg A_\vee \vee A_\wedge \vee z)}\\
                    &\alert{\wedge (\neg A_\wedge \vee x) \wedge (\neg A_\wedge \vee y)} \\
                    &\qquad\alert{\wedge(A_\wedge \vee \neg x \vee \neg y)}}
            \end{align}
        \end{column}
        \begin{column}{.3\textwidth}
            \begin{tikzpicture}[grow=down, level distance = 33]
                \tikzstyle{op} = [pretty]
                \tikzstyle{var} = [pretty, rectangle]
                \tikzstyle{edge from parent} = [edge]

                \tikzstyle{level 1} = [sibling distance = 50]
                \tikzstyle{level 2} = [sibling distance = 30]
                \node at (0, 0) {};
                \node[op] at (0, -1) {\alt<1>{$\vee$}{$A_\vee$}}
                child {
                    node[op] {\alt<1>{$\wedge$}{$A_\wedge$}}
                    edge from parent
                    child {
                        node[var] {$x$}
                        edge from parent
                    }
                    child {
                        node[var] {$y$}
                        edge from parent
                    }
                }
                child {
                    node[var] {$z$}
                };
            \end{tikzpicture}
        \end{column}
    \end{columns}
\end{frame}

\begin{frame}
    \frametitle{DPLL}
    \setbeamercovered{dynamic}

    \begin{definition}[DPLL-Belegung]
        Sei $F$ eine Formel in KNF und $p$ eine Variable von $F$.\\
        Dann bezeichnet \structure{$F[p\backslash\true]$} die Formel, die entsteht, wenn jedes Vorkommnis von $p$ in F durch $\true$ ersetzt und vereinfacht wird.
    \end{definition}

    \begin{block}{DPLL}
        Gegeben eine Formel $F$ in KNF
        \begin{itemize}
            \item Wenn $F = \true$ dann antworte \structure{erfüllbar}
            \item Wenn $F = \false$ dann antworte \structure{unerfüllbar}
            \item Sonst
                \begin{enumerate}
                    \item Wähle eine Variable $p$ in $F$
                    \item Prüfe ob $F[p\backslash\true]$ oder $F[p\backslash\false]$ erfüllbar
                \end{enumerate}
        \end{itemize}
    \end{block}
    \begin{itemize}
        \item Schlaue Wahl der Variable beschleunigt Ausführung
        \item Wähle Variablen die einzeln stehen (\structure{One-Literal-Rule})
    \end{itemize}
\end{frame}
}

\defineUnit{resolution}{%
\begin{frame}
    \frametitle{Resolution}
    \setbeamercovered{dynamic}

    \begin{definition}[Resolvent]
        Seien $K_1$, $K_2$ und $R$ Klauseln in Mengendarstellung. Dann heißt $R$ \structure{Resolvent} von $K_1$ und $K_2$ wenn $L \in K_1$, $\neg L \in K_2$ und
        \begin{align}
            R &= \left( K_1 \setminus \left\{ L \right\} \right) \cup \left( K_2 \setminus \left\{ \neg L \right\} \right)
        \end{align}
    \end{definition}

    \begin{block}{Resolution}
        Gegeben eine Formel $F$ in KNF in Mengendarstellung.
        \begin{algorithmic}
            \While{$\square = \emptyset \not \in F$}
                \State{$R \gets \text{Resolvent aus } F \text{ mit } R \not\in F$}
                \If{$R$ existiert}
                    \State{$F \gets F \cup R$}
                \Else
                    \State{\textbf{return} \structure{erfüllbar}}
                \EndIf
            \EndWhile
            \State{\textbf{return} \structure{unerfüllbar}}
        \end{algorithmic}
    \end{block}
\end{frame}
}

\defineUnit{kalkuele}{%
\begin{frame}
    \frametitle{Kalküle}
    \setbeamercovered{dynamic}

    \begin{definition}[Kalkül]
        Ein \structure{Logikkalkül} stellt \structure{Inferenzregeln} bereit, mit denen Formeln \alert{syntaktisch} umgeformt werden können.
    \end{definition}

    \begin{definition}[Folgerung]
        $F$ \structure{folgt aus} $A$, wenn mit Hilfe der \alert{Semantik} der \alert{Aussagenlogik} $F$ unter der Annahme dass $A$ gilt zu $\true$ ausgewertet wird. Wir schreiben
        \[ A \vDash F \]
    \end{definition}

    \begin{definition}[Ableitung]
        $F$ kann aus $A$ \structure{abgeleitet} werden, wenn mit Hilfe \alert{syntaktischer} Umformungen in einem \alert{Logikkalkül} $F$ unter der Annahme $A$ bewiesen werden kann. Wir schreiben
        \[ A \vdash F \]
    \end{definition}
\end{frame}

\begin{frame}
    \frametitle{Eigenschaften von Kalkülen}
    \setbeamercovered{dynamic}

    \begin{block}{Eigenschaften von Kalkülen}
        \begin{description}[\quad vollständig (complete)]
            \item[korrekt (sound)] Es können \alert{nur} semantisch gültige Formeln abgeleitet werden.
                \[ \text{Aus } A \vdash F \text{ folgt } A \vDash F \]
            \item[vollständig (complete)] \alert{Alle} semantisch gültigen Formeln können abgeleitet werden.
                \[ \text{Aus } A \vDash F \text{ folgt } A \vdash F \]
        \end{description}
    \end{block}

    \begin{itemize}
        \item Für uns nur korrekte vollständige Kalküle
        \item Beispiel für die Aussagenlogik: \structure{Natürliches Schließen}
            \medskip
        \item Es gibt keine solchen Kalküle für die
            \begin{itemize}
                \item Prädikatenlogik
                \item Arithmetik
            \end{itemize}
        \item Deshalb sind nicht alle Sätze der Mathematik beweisbar
    \end{itemize}
\end{frame}
}

\defineUnit{natuerlichesschliessen}{%
{
    \newcommand{\F}{\tau}
    \newcommand{\G}{\varphi}
    \newcommand{\K}{\chi}
    \newcommand{\subproof}[2]{%
        \begin{tikzpicture}[y=.9em]
            \path
            (0, 0) node (a) {##1}
            ++(0, -1) node (b) {$\vdots$}
            ++(0, -1) node[below] (c) {##2};
            \node[fit=(a)(b)(c), draw, inner sep=1pt] {};
        \end{tikzpicture}%
    }
    \newcommand{\topproof}[1]{%
        ##1
        \bottomAlignProof
        \DisplayProof
    }
    \newcommand{\capt}[1]{\vspace{-1em}##1}

    \begin{frame}
        \frametitle{Natürliches Schließen}
        \setbeamercovered{dynamic}

        \tabulinesep=4pt
        \begin{tabu} to \textwidth {X[c,m,.5]|[1pt]X[c,b,5]X[c,b,5]}
            & \structure{Introduktion} & \structure{Elimination}\\\tabucline[1pt]{-}
            \capt{$\wedge$} &
                \topproof{
                    \AxiomC{$\F$}
                    \AxiomC{$\G$}
                    \RightLabel{\scriptsize $+\wedge$}
                    \BinaryInfC{$\F \wedge \G$}
                }
            &
                \topproof{
                    \AxiomC{$\F \wedge \G$}
                    \RightLabel{\scriptsize $-\wedge_1$}
                    \UnaryInfC{$\F$}
                }
                \quad
                \topproof{
                    \AxiomC{$\F \wedge \G$}
                    \RightLabel{\scriptsize $-\wedge_2$}
                    \UnaryInfC{$\G$}
                }
            \\
            \capt{$\vee$} &
                \topproof{
                    \AxiomC{$\F$}
                    \RightLabel{\scriptsize $+\vee_1$}
                    \UnaryInfC{$\F \vee \G$}
                }
                \quad
                \topproof{
                    \AxiomC{$\G$}
                    \RightLabel{\scriptsize $+\vee_2$}
                    \UnaryInfC{$\F \vee \G$}
                }
            &
                \topproof{
                    \AxiomC{$\F \vee \G$}
                    \AxiomC{\subproof{$\F$}{$\K$}}
                    \AxiomC{\subproof{$\G$}{$\K$}}
                    \RightLabel{\scriptsize $-\vee$}
                    \TrinaryInfC{$\K$\vphantom{$\F\G$}}
                }
            \\
            \capt{$\rightarrow$} &
                \topproof{
                    \AxiomC{\subproof{$\F$}{$\G$}}
                    \RightLabel{\scriptsize $+\rightarrow$}
                    \UnaryInfC{$\F \rightarrow \G$}
                }
            &
                \topproof{
                    \AxiomC{$\F$}
                    \AxiomC{$\F \rightarrow \G$}
                    \RightLabel{\scriptsize $-\rightarrow$, MP}
                    \BinaryInfC{$\G$}
                }
            \\
            \capt{$\neg$} &
                \topproof{
                    \AxiomC{\subproof{$\F$}{$\bot$}}
                    \RightLabel{\scriptsize $+\neg$}
                    \UnaryInfC{$\neg \F$}
                }
            &
                \topproof{
                    \AxiomC{$\F$}
                    \AxiomC{$\neg\F$}
                    \RightLabel{\scriptsize $-\neg$}
                    \BinaryInfC{$\bot$}
                }
        \end{tabu}
    \end{frame}

    \begin{frame}
        \frametitle{Natürliches Schließen}
        \setbeamercovered{dynamic}

        \tabulinesep=4pt
        \begin{tabu} to \textwidth {X[c,m,.5]|[1pt]X[c,b,5]X[c,b,5]}
            & \structure{Introduktion} & \structure{Elimination}\\\tabucline[1pt]{-}
            \capt{$\bot$} &
            &
                \topproof{
                    \AxiomC{$\bot$}
                    \RightLabel{\scriptsize $-\bot$}
                    \UnaryInfC{$\F$}
                }
            \\
            \capt{$\neg\neg$} &
                \topproof{
                    \AxiomC{$\F$}
                    \RightLabel{\scriptsize $+\neg\neg$}
                    \UnaryInfC{$\neg\neg\F$}
                }
            &
                \topproof{
                    \AxiomC{$\neg\neg\F$}
                    \RightLabel{\scriptsize $-\neg\neg$}
                    \UnaryInfC{$\F$}
                }
        \end{tabu}
        \begin{itemize}
                \vfill
            \item Praktische abgeleitete Regeln
        \end{itemize}
        \tabulinesep=10pt
        \begin{tabu} to \textwidth {X[c,m,.5]X[c,b,5]X[c,b,5]}
            &
                \topproof{
                    \AxiomC{ }
                    \RightLabel{\scriptsize LEM}
                    \UnaryInfC{$\F \vee \neg\F$}
                }
            &
                \topproof{
                    \AxiomC{\subproof{$\neg\F$}{$\bot$}}
                    \RightLabel{\scriptsize $-\neg$, PBC}
                    \UnaryInfC{$\F$}
                }
            \\
            &
            &
                \topproof{
                    \AxiomC{$\neg\G$}
                    \AxiomC{$\F \rightarrow \G$}
                    \RightLabel{\scriptsize MT}
                    \BinaryInfC{$\neg\F$}
                }
        \end{tabu}
    \end{frame}
}
}

\defineUnit{praedikatenlogiksyntax}{%
{
    \newcommand{\terms}{\mathcal{T}}
    \newcommand{\preds}{\mathcal{P}}
    \newcommand{\logic}{\mathcal{L}}
    \begin{frame}[c]
        \frametitle{Syntax der Prädikatenlogik}
        \setbeamercovered{dynamic}

        \begin{definition}[Term]
            Die Menge $\terms$ aller \structure{Terme} ist induktiv definiert.
            \begin{itemize}
                \item Jede Konstante ist in $\terms$
                \item Jede Variable ist in $\terms$
                \item Sind $f$ eine Funktion und $t_1, \dots, t_n$ Terme, dann auch
                    \[ f(t_1, \dots, t_n) \]
            \end{itemize}
            Funktionen wandeln Terme in \alert{Terme} um. Wir beschreiben sie mit Kleinbuchstaben.
        \end{definition}

        \begin{definition}[Prädikat]
            \structure{Prädikate} $P$ wandeln Terme in \alert{Wahrheitswerte} um.
            Wir beschreiben sie mit Großbuchstaben.\\
            Die Menge $\preds$ enthält alle \structure{Prädikate}.
        \end{definition}
    \end{frame}

    \begin{frame}[c]
        \frametitle{Syntax der Prädikatenlogik}
        \setbeamercovered{dynamic}

        \begin{definition}[Syntax der Prädikatenlogik]
            Die Menge \structure{$\logic$} aller \structure{prädikatenlogischen Formeln} ist induktiv definiert.
            Seien $A, B\in \logic$, $t_i \in \terms$ und $P \in \preds$. Dann sind alle Formeln
            {
                \setlength{\belowdisplayskip}{0pt}
                \setlength{\abovedisplayskip}{0pt}
                \begin{itemize}
                        \item Grundbausteine
                            \smallskip
                        \begin{align}
                            V = \left\{ a, b, \dots \right\} &\subseteq \logic\tag{\alert{Variablen}}\\
                            P(t_1, \dots, t_n) &\in \logic\tag{\alert{Prädikate, Konstanten}}\\
                            t_i = t_j &\in\logic\tag{\alert{Gleichheit}}\\
                            \shortintertext{\item Verknüpfungen der Aussagenlogik}
                            \neg A &\in \logic\tag{\alert{Negation}}\\
                            (A \wedge B), (A \vee B)&\in \logic\tag{\alert{Konjunktion, Disjunktion}}\\
                            (A \rightarrow B)&\in \logic\tag{\alert{Implikation}}\\
                            \shortintertext{\item \structure{Quantoren}}
                            \exists x. A &\in \logic\tag{\alert{Existenzquantor}}\\
                            \forall x. A &\in \logic\tag{\alert{Allquantor}}\\
                        \end{align}
                \end{itemize}
            }
            \vspace{-1.5em}
        \end{definition}
    \end{frame}

    \begin{frame}
        \frametitle{Operatorenbindung}
        \setbeamercovered{dynamic}

        \begin{definition}[Bindungsregeln]
            Die \structure{Bindungsstärke} der Operatoren in absteigender Reihenfolge ist
            \[ \forall \quad \exists \quad \neg \quad \wedge \quad \vee \quad \rightarrow \quad \leftrightarrow \]
            Die Implikation ist \structure{rechtsassoziativ}.
        \end{definition}
        \begin{itemize}
            \item Üblicherweise klammert man wieder $\wedge$ und $\vee$
            \item Genauso klammert man Quantoren
                \[ \left( \forall x. F \right) \rightarrow G \text{\quad statt\quad} \forall x. F \rightarrow G \]
            \vfill
            \item \alert{Achtung!} Äußere Quantoren werden öfter anders interpretiert
                \[ \forall x \forall y. F \wedge G \leftrightarrow H \]
                Bindet formal \alert{nur an das F}!
        \end{itemize}
    \end{frame}
}
}

\defineUnit{praedikatenlogikstruktur}{%
\begin{frame}[c]
    \frametitle{Struktur}
    \setbeamercovered{dynamic}

    \begin{definition}[Struktur]
        Eine passende \structure{Struktur} $S = \left( U_s, I_s \right)$ zu einer Formel $F$ besteht aus einem \structure{Universum} $U_s$ und einer \structure{Interpretation} $I_s$.
        \begin{itemize}
            \item Alle Terme werten zu einem Wert im \structure{Universum} $U_s$ aus
            \item Die \structure{Interpretation} $I_s$ weist den Atomen der Formel Werte zu.\\
                Sie spezifiziert
                \begin{itemize}
                    \item \alert{Variablen} $x$ mit
                        {
                            \setlength{\belowdisplayskip}{0pt}
                            \setlength{\abovedisplayskip}{0pt}
                            \begin{align}
                                x_s \in {} &U_s\\
                            \shortintertext{\item \alert{Konstanten} $a$ mit}
                                a_s \in {} &U_s\\
                            \shortintertext{\item \alert{k-stellige Prädikate} $P$ mit}
                                P_s \subseteq {} &U_s^k\\
                            \shortintertext{\item \alert{Funktionen} $f$ mit}
                                f_s : {} &U_s^k \to U_s
                            \end{align}
                        }
                \end{itemize}
        \end{itemize}
    \end{definition}
\end{frame}
}
