181 lines
9.8 KiB
TeX
181 lines
9.8 KiB
TeX
\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} |