diff --git a/chapters/Logik/Prädikatenlogik.tex b/chapters/Logik/Prädikatenlogik.tex new file mode 100644 index 0000000..75f0d94 --- /dev/null +++ b/chapters/Logik/Prädikatenlogik.tex @@ -0,0 +1,165 @@ +\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 = \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 = \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 ($\rightleftarrows$) vollständig beseitigen. + Ggfs. Schritt 1 wiederholen + \item Mit \say{de Morganschen Gesetzen} 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 = .8\textwidth]{pränexform_äquivalenzen.png}\\ + {\Large\color{red}ABER!!}\\ + \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*} + + \subsubsection{Beispiele} + \label{praenexform: beispiele} + \includegraphics[width = .8\textwidth]{pränexform_beispiele.png} + + \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{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} + \includegraphics[width = .8\textwidth]{prädikatenlogik_resolutionsalgorithmus.png} \ No newline at end of file diff --git a/images/prädikatenlogik_1_stufe.png b/images/prädikatenlogik_1_stufe.png new file mode 100644 index 0000000..4b7f052 Binary files /dev/null and b/images/prädikatenlogik_1_stufe.png differ diff --git a/images/prädikatenlogik_1_stufe2.png b/images/prädikatenlogik_1_stufe2.png new file mode 100644 index 0000000..7386fb5 Binary files /dev/null and b/images/prädikatenlogik_1_stufe2.png differ diff --git a/images/prädikatenlogik_1_stufe_funktionen.png b/images/prädikatenlogik_1_stufe_funktionen.png new file mode 100644 index 0000000..64f9944 Binary files /dev/null and b/images/prädikatenlogik_1_stufe_funktionen.png differ diff --git a/images/prädikatenlogik_1_stufe_mögliche_welten.png b/images/prädikatenlogik_1_stufe_mögliche_welten.png new file mode 100644 index 0000000..d0510a6 Binary files /dev/null and b/images/prädikatenlogik_1_stufe_mögliche_welten.png differ diff --git a/images/prädikatenlogik_1_stufe_relationen.png b/images/prädikatenlogik_1_stufe_relationen.png new file mode 100644 index 0000000..fe7e3ca Binary files /dev/null and b/images/prädikatenlogik_1_stufe_relationen.png differ diff --git a/images/prädikatenlogik_1_stufe_wahrheit_allquantor.png b/images/prädikatenlogik_1_stufe_wahrheit_allquantor.png new file mode 100644 index 0000000..dc7f82b Binary files /dev/null and b/images/prädikatenlogik_1_stufe_wahrheit_allquantor.png differ diff --git a/images/prädikatenlogik_1_stufe_wahrheit_existenzquantor.png b/images/prädikatenlogik_1_stufe_wahrheit_existenzquantor.png new file mode 100644 index 0000000..8f1afb3 Binary files /dev/null and b/images/prädikatenlogik_1_stufe_wahrheit_existenzquantor.png differ diff --git a/images/prädikatenlogik_formale_sprache.png b/images/prädikatenlogik_formale_sprache.png new file mode 100644 index 0000000..158ccec Binary files /dev/null and b/images/prädikatenlogik_formale_sprache.png differ diff --git a/images/prädikatenlogik_inferenzregeln.png b/images/prädikatenlogik_inferenzregeln.png new file mode 100644 index 0000000..560adc3 Binary files /dev/null and b/images/prädikatenlogik_inferenzregeln.png differ diff --git a/images/prädikatenlogik_resolutionsalgorithmus.png b/images/prädikatenlogik_resolutionsalgorithmus.png new file mode 100644 index 0000000..7579a46 Binary files /dev/null and b/images/prädikatenlogik_resolutionsalgorithmus.png differ diff --git a/images/pränexform_beispiele.png b/images/pränexform_beispiele.png new file mode 100644 index 0000000..4ec85a3 Binary files /dev/null and b/images/pränexform_beispiele.png differ diff --git a/images/pränexform_äquivalenzen.png b/images/pränexform_äquivalenzen.png new file mode 100644 index 0000000..f09c36f Binary files /dev/null and b/images/pränexform_äquivalenzen.png differ diff --git a/images/skolemisierung_beispiel.png b/images/skolemisierung_beispiel.png new file mode 100644 index 0000000..a3ba4ae Binary files /dev/null and b/images/skolemisierung_beispiel.png differ diff --git a/images/unifikation_beispiel.png b/images/unifikation_beispiel.png new file mode 100644 index 0000000..0d90f0a Binary files /dev/null and b/images/unifikation_beispiel.png differ diff --git a/parts/Logik.tex b/parts/Logik.tex index 5818030..eed2569 100644 --- a/parts/Logik.tex +++ b/parts/Logik.tex @@ -4,4 +4,5 @@ \input{chapters/Logik/Formen der Inferenz.tex} \input{chapters/Logik/Logische Systeme.tex} \input{chapters/Logik/Aussagenlogik.tex} -\input{chapters/Logik/Beweisverfahren.tex} \ No newline at end of file +\input{chapters/Logik/Beweisverfahren.tex} +\input{chapters/Logik/Prädikatenlogik.tex} \ No newline at end of file