diff --git a/chapters/Logik/Beweisverfahren.tex b/chapters/Logik/Beweisverfahren.tex
index 5b26052..10d97f1 100644
--- a/chapters/Logik/Beweisverfahren.tex
+++ b/chapters/Logik/Beweisverfahren.tex
@@ -48,4 +48,30 @@
         \subsection{Resolutionsalgorithmus}
         \label{resolutionsalgorithmus}
             \includegraphics[width = .8\textwidth]{resolutionsalgorithmus1.png}\\
-            \includegraphics[width = .3\textwidth]{resolutionsalgorithmus2.png}
\ No newline at end of file
+            \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}
\ No newline at end of file
diff --git a/images/backward_chaining.png b/images/backward_chaining.png
new file mode 100644
index 0000000..625f0dc
Binary files /dev/null and b/images/backward_chaining.png differ
diff --git a/images/forward_chaining.png b/images/forward_chaining.png
new file mode 100644
index 0000000..14f24b4
Binary files /dev/null and b/images/forward_chaining.png differ