\chapter{Beweisverfahren}
\label{logik: beweisverfahren}
    \section{Logische Folgerung}
    \label{logische folgerung}
        $$\models \subseteq Formel(\Sigma)\times Formel(\Sigma)$$
        $$ F \models G: \text{Aus }F\text{ folgt logisch }G$$
        $$ F \models G \text{ gdw. } Mod(F)\subseteq Mod(G)$$
        \includegraphics[width = .8\textwidth]{folgerung.png}\\
        Hieraus lässt sich ein automatisiertes Beweisverfahren entwickeln, indem überprüft wird, ob in jeder Welt, ind der $F$ war ist auch $G$ war ist.

    \section{Widerspruchsbeweis}
    \label{widerspruchsbeweis}
        $$F\models G \text{ gdw. }F\wedge\neg G \text{ unerfüllbar}$$
        Hieraus lässt sich ein automatisiertes Beweisverfahren aufstellen, indem $\neg G$ zu $F$ hinzugefügt wird und daraus ein Widerspruch abgeleitet wird.

    \section{Inferenz}
    \label{inferenz}
        $$F\models G$$
        Dies ist auf 2 Arten beweisbar:
        \begin{enumerate}
            \item \textbf{Modellüberprüfung:}\\
                Überprüfung, ob in allen Welten, in denen $F$ war ist auch $G$ war ist
            \item \textbf{Theoreme beweisen:}\\
                Abfolge von Beweisschritten (Inferenzregeln(\ref{inferenzregeln})) von $WB$ nach $F$
        \end{enumerate}

        \subsection{Inferenzalgorithmen}
        \label{inferenzalgorithmen}
            \includegraphics[width = \textwidth]{inferenzalgorithmen.png}

        \subsection{Inferenzregeln}
        \label{inferenzregeln}
           \includegraphics[width = .8\textwidth]{inferenzregeln.png} 

        \subsection{Beweis durch Resolution}
        \label{beweis durch resolution}
            $$\frac{A\vee B, \neg B\vee C}{A\vee C}$$

        \subsection{Allgemeine Resolutionsregel}
        \label{allgemeine resolutionsregel}
            $$\frac{(A_1\vee \dots \vee A_m\vee B), (\neg B \vee C_1 \vee\dots\vee C_n)}{(A_1\vee\dots\vee A_m\vee C_1\vee\dots\vee C_n)}$$

        \subsection{Klauselform}
        \label{klauselform}
            Die Klauselform ist die Mengendarstellung der \ac{KNF}:\\
            \includegraphics[width = \textwidth]{klauselform.png}

        \subsection{Resolutionsalgorithmus}
        \label{resolutionsalgorithmus}
            \includegraphics[width = .8\textwidth]{resolutionsalgorithmus1.png}\\
            \includegraphics[width = .3\textwidth]{resolutionsalgorithmus2.png}