\chapter{Prädikatenlogik}
\label{praedikatenlogik}
    Da es viele reale Eigenschaften gibt, die mit Aussagenlogik (\ref{aussagenlogik}) schwer auszudrücken sind wird hier die Prädikatenlogik verwendet.

    \section{Festlegung formaler Sprache}
    \label{praedikatenlogik: formale sprache}
        \includegraphics[width=\textwidth]{prädikatenlogik_formale_sprache.png}

    \section{Prädikatenlogik 1.Stufe}
    \label{praedikatenlogik: 1.stufe}
        \includegraphics[width = .8\textwidth]{prädikatenlogik_1_stufe.png}\\
        \includegraphics[width = .8\textwidth]{prädikatenlogik_1_stufe2.png}

        \subsection{Signatur $\Sigma$}
        \label{prae. 1.stufe: signatur}
            $$\Sigma =  (Func,Pred)$$
            \begin{itemize}
                \item $Func$: Menge von Funktionssymbolen bestimmter Stelligkeit
                \item $Pred$: Menge von Prädikatensymbolen bestimmter Stelligkeit
            \end{itemize}

        \subsection{Interpretation $I$}
        \label{prae. 1.stufe: interpretation}
            \begin{itemize}
                \item Konstante und Variablen $\rightarrow$ Objekte aus der Welt, Trägermenge $U_I$
                \item Menge der Funktionssymbole $\rightarrow$ Menge der Funktionen der Welt
                \item Menge der Prädikatensymbole $\rightarrow$ Menge der Relationen der Welt
            \end{itemize}

        \subsection{Mögliche Welten}
        \label{prae. 1.stufe: moegliche welten}
            \includegraphics[width = .9\textwidth]{prädikatenlogik_1_stufe_mögliche_welten.png}

        \subsection{Funtionssymbole}
        \label{prae. 1.stufe: funktionssymbole}
            \begin{itemize}
                \item \textbf{Nullstellige} Funktionssymbole werden durch Objekte der betrachteten Welt interpretiert
                \item \textbf{Mehrstellige} Funktionssymbole werden durch Funktionen interpretiert
            \end{itemize}

        \subsection{Funktionen}
        \label{prae. 1.stufe: funktionssymbole}
            \includegraphics[width = .9\textwidth]{prädikatenlogik_1_stufe_funktionen.png}

        \subsection{Prädikatensymbole}
        \label{prae. 1.stufe: praedikatensymbole}
            \begin{itemize}
                \item \textbf{Nullstellige} Prädikatensymbole werden wie \textbf{Aussagenvariablen} (\ref{aussagenlogik}) interpretiert
                \item \textbf{Einstellige} Prädikatensymbole werden als Menge aller Dinge denen eine bestimmte Eigenschaft zukommt interpretiert
                \item \textbf{Mehrstellige} Prädikatensymbole werden als \textbf{Relationen} (\ref{prae. 1.stufe: relationen}) interpretiert
            \end{itemize}

        \subsection{Relationen}
        \label{prae. 1.stufe: relationen}
            \includegraphics[width = \textwidth]{prädikatenlogik_1_stufe_relationen.png}

        \subsection{Wahrheitsbegriff}
        \label{prae. 1.stufe: wahrheitsbegriff}
            \begin{itemize}
                \item Atomare Formel $p(t_1,\dots,t_n)$ wahr unter $I$, wenn mit Interpretation des Prädikats $p$ durch eine Relation diese Relation unter $I$ für $t_1,\dots,t_n$ gilt.
                \item ie Wahrheit quantorenfreier Formeln ergibt sich aus Semantik der logischen Operatoren (wie in der Aussagenlogik (\ref{aussagenlogik})).
            \end{itemize}

            \subsubsection{Wahrheit des Allquantors}
            \label{prae. 1.stufe: wahrheit des allquantors}
                \includegraphics[width = \textwidth]{prädikatenlogik_1_stufe_wahrheit_allquantor.png}

            \subsubsection{Wahrheit des Existenzquantors}
            \label{prae. 1.stufe: wahrheit des existenzquantors}
                \includegraphics[width = \textwidth]{prädikatenlogik_1_stufe_wahrheit_existenzquantor.png}

    \section{Normalformen}
    \label{praedikatenlogik: normalformen}
        \subsection{Pränexform}
        \label{praedikatenlogik: praenexform}
            Das Ziel der Pränexform ist es eine Normalform zu haben, die möglichst wenig Quantoren beinhaltet,
            da die Quantoren für die automatische Interferenz hinderlich sind.
            Die Pränexform definiert sich allgemein durch:
            $$F = Q_1x_1\dots Q_nx_n\hat{F}$$
            Hierbei ist $\hat{F}$ quantorenfrei und $Q_i\in\{\forall,\exists\} \text{ für } i=1,\dots,n$.

            \subsubsection{Umstellung}
            \label{umstellung praenexform}
                Jeder Formel lässt sich in die Pränexform umstellen.
                \begin{enumerate}
                    \item Variablenumbenennung: Hinter allen Quantoren müssen verschiedene Variablen stehen.
                    \item Implikation ($\Rightarrow$) und Äquvivalenz ($\Leftrightarrow$) vollständig beseitigen.
                        Ggfs. Schritt 1 wiederholen
                    \item Mit \say{de Morganschen Gesetzen} (\ref{aussagenlogik: aequivalenzen}) und
                        $$ \neg\forall x F \equiv \exists x\neg F$$
                        $$ \neg\exists x F \equiv \forall x\neg F$$
                        Negationszeichen nach ganz innen schieben.
                    \item Quantoren unter Beachtung der Äquivalenzen ganz nach außen schieben.
                \end{enumerate}

                \paragraph{Äquivalenzen}\mbox{}\\
                    \includegraphics[width = \textwidth]{pränexform_äquivalenzen.png}\\
                    {\Large\color{red}ABER!!}\\
                    \large
                    \begin{align*}
                        (\forall x F) \vee (\forall x G)&\not\equiv \forall x (F\vee G)\\
                        (\exists x F) \wedge (\exists x G)&\not\equiv \exists x (F\wedge G)
                    \end{align*}
                    \normalsize

            \subsubsection{Beispiele}
            \label{praenexform: beispiele}
                \includegraphics[width = \textwidth]{pränexform_beispiele.png}
\pagebreak
                
        \subsection{Skolemisierung}
        \label{skolemisierung}
            Bei der Skolemisierung wird durch die Elimination der Existenzquantoren eine formel erstellt, die zwar \textbf{nicht semantisch äquivalent},
            aber immer noch \textbf{erfüllbarkeitsäquivalent} ist.

            \subsubsection{Verfahren}
            \label{skolemisierung: verfahren}
                \begin{enumerate}
                    \item Funktion in Pränexform umstellen
                    \item Alle Existenzquantoren $\exists$ weglassen
                    \item Falls Existenzquantoren $\exists$ vor Allquantoren $\forall$:\\
                        Variablen der Existenzquantoren durch Konstanten ersetzen
                    \item Falls Existenzquantor $\exists$ hinter einem oder mehreren Allquantoren $\forall$:\\
                        Variablen der Existenzquantoren durch Skolemfunktionen ersetzen.
                        Diese beinhalten jeweils die Variablen der Allquantoren $\forall$ von denen sie abhängen.
                \end{enumerate}

            \subsubsection{Beispiel}
            \label{skolemisierung: beispiel}
                \includegraphics[width = .8\textwidth]{skolemisierung_beispiel.png}

        \subsection{Erfüllbarkeitsäquivalente Normalform}
        \label{erfuellbarkeitsaequivalente normalform}
            Durch die folgenden Schritte wird eine erfüllbarkeitsäquivalente \ac{KNF} erreicht:
            \begin{enumerate}
                \item Transformation in die Pränexform (\ref{praedikatenlogik: praenexform})
                \item Skolemisierung (\ref{skolemisierung})
            \end{enumerate}

    \section{Inferenzregeln}
    \label{praedikatenlogik: inferenzregeln}
        Wie schon bei den Aussagenlogik (\ref{aussagenlogik}) lassen sich auf für die Prädikatenlogik Inferenzregeln definieren.
        $$ F\models G \text{ gdw. } F\Rightarrow G\text{ ist tautologisch}$$
        Widerspruchsbeweis:
        $$ F\models G \text{ gdw. } F\wedge\neg G\text{ ist unerfüllbar}$$
        \includegraphics[width = .8\textwidth]{prädikatenlogik_inferenzregeln.png}

    \section{Resolution}
    \label{praedikatenlogik: resolution}
        Wie bei der Aussagenlogik (\ref{aussagenlogik}) gilt auch bei der Prädikatenlogik das gleiche Prinzip für die Resolution:
        \begin{itemize}
            \item $\neg Q$ zur Wissensbasis hinzufügen
            \item Ziel: Leere Klausel ableiten
            \item Wichtig: Wissensbasis muss widerspruchsfrei sein!
        \end{itemize}
        Der Unterschied zur Aussagenlogik besteht darin, dass die Terme Variablen erhalten.
        Zudem müssen die Literalte zur Durchführung des Resolutionsschritts angeglichen werden.

    \section{Unifikation}
    \label{praedikatenlogik: unifikation}
        Bei der Unifizierung werden die Variablen zweier Terme angeglichen.
        Der \textbf{allgemeinste Unifikator} ist der, der am wenigsten Einschränkungen an den Variablen vornimmt.
        Dieser kann als Schnittmenge der Modelle interpretiert werden.
        
        \subsection{Beispiel}
        \label{unifikation:beispiel}
            \includegraphics[width = .8\textwidth]{unifikation_beispiel.png}

    \section{Allgemeine Resolutionsregel}
    \label{praedikatenlogik: allgemeine resolutionsregel}
        Die allgemeine Resolutionsregel lautet:
        $$\frac{\{A_1,\dots,A_n,B\},\{\neg B,C_1,\dots,C_m\}~\sigma(B)=\sigma(\neg B)}{\{\sigma(A_1),\dots,\sigma(A_n),\sigma(C_1),\dots,\sigma(C_m)\}}$$
        Wobei $\sigma$ der allgemeinste Unifikator von $B$ und $\neg B$ ist.\\
        Zusammen mit der Faktorisierungsregel
        $$\frac{\{A_1,\dots,A_n,B,B'\}~\sigma(B)=\sigma(B')}{\{\sigma(A_1),\dots,\sigma(A_n),\sigma(B)\}}$$
        ergibt die Resolutionsregel ein vollständige Inferenzregel

    \section{Resolutionsalgorithmus}
    \label{praedikatenlogik: resolutionsalgorithmus}
        Wie bei der Aussagenlogik muss für die Resolution die negierte Hypothese der Wissensbasis hinzugefügt werden (\ref{resolutionsalgorithmus}).\\
        \includegraphics[width = .8\textwidth]{prädikatenlogik_resolutionsalgorithmus.png}