\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}

    \section{Hornklauseln}
    \label{hornklauseln}
        Klauseln in \ac{KNF} lassen sich nach positiven und negativen Literalen sortieren:
        $$ (\neg A_1\vee\dots\vee\neg A_m\vee B_1\vee\dots\vee B_n)$$
        Hieraus ergibt sich durch umformen:
        $$ A_1\wedge\dots\wedge A_m \Rightarrow B_1\vee\dots\vee B_n$$
        Dies ist besonders hilfreich, wenn die Klausel nur ein positives Literal enthält:
        $$ \neg A_1\vee\dots\vee\neg A_m\vee B)$$
        $$A_1\wedge\dots\wedge A_m \Rightarrow B$$
        Diese Klauseln werden als \textbf{Hornklauseln} bezeichnet.
        Der große Vorteil bei der Nutzung von Hornklauseln ist,
        dass die Laufzeit einer Folgerung mit Hornklauseln \textbf{linear} in der Anzahl der Fakten der Wissensbasis ist.

        \subsection{Forward Chaining}
        \label{forward chaining}
            Der Modus Ponens (\ref{inferenzregeln}) ist für Hornklauseln eine vollständige Inferenzregel:
            $$\frac{A_1\wedge\dots\wedge A_m, A_1\wedge\dots\wedge A_m \Rightarrow B}{B}$$
            \includegraphics[width = \textwidth]{forward_chaining.png}

        \subsection{Backward Chaining}
        \label{backward chaining}
            Während das Forward Chaining (\ref{forward chaining}) den einen datengetriebenen Ansatz verfolgt (Bei den Fakten starten und Anfrage herleiten)
            beginnt das Backward Chaining bei der Anfrage und arbeitet die relevanten Teile des Und-Oder-Graphen rückwärts ab.
            Dies hat den Vorteil, das anders als beim Forward Chaining keine potentiell unnötigen Formeln abgeleitet werden.\\
            \includegraphics[width = \textwidth]{backward_chaining.png}