94 lines
4.6 KiB
TeX
94 lines
4.6 KiB
TeX
\chapter{Beweisverfahren}
|
|
\label{logik: beweisverfahren}
|
|
\section{Logische Folgerung}
|
|
\label{logische folgerung}
|
|
\begin{wrapfigure}[10]{r}{.5\textwidth}
|
|
\vspace{-10mm}
|
|
\includegraphics[width = .5\textwidth]{folgerung.png}
|
|
\end{wrapfigure}
|
|
$$\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)$$
|
|
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}
|
|
\begin{center}
|
|
\includegraphics[width = .6\textwidth]{inferenzregeln.png}
|
|
\end{center}
|
|
|
|
\subsection{Beweis durch Resolution}
|
|
\label{beweis durch resolution}
|
|
\Large
|
|
$$\frac{A\vee B, \neg B\vee C}{A\vee C}$$
|
|
\normalsize
|
|
|
|
\subsection{Allgemeine Resolutionsregel}
|
|
\label{allgemeine resolutionsregel}
|
|
\Large
|
|
$$\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)}$$
|
|
\normalsize
|
|
|
|
\subsection{Klauselform}
|
|
\label{klauselform}
|
|
Die Klauselform ist die Mengendarstellung der \ac{KNF}:\\
|
|
\includegraphics[width = .7\textwidth]{klauselform.png}
|
|
|
|
\subsection{Resolutionsalgorithmus}
|
|
\label{resolutionsalgorithmus}
|
|
\begin{center}
|
|
\includegraphics[width = .6\textwidth]{resolutionsalgorithmus1.png}\\
|
|
Die Hypothese wird der Wissensbasis negiert hinzugefügt.
|
|
Falls sich die Klausel dann zur leeren Menge ableiten lässt ist die Hypothese bewiesen.\\
|
|
\includegraphics[width = .2\textwidth]{resolutionsalgorithmus2.png}
|
|
\end{center}
|
|
|
|
\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}$$
|
|
\begin{center}
|
|
\includegraphics[width = .6\textwidth]{forward_chaining.png}
|
|
\end{center}
|
|
|
|
\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.\\
|
|
\begin{center}
|
|
\includegraphics[width = .6\textwidth]{backward_chaining.png}
|
|
\end{center} |