diff --git a/Acronyms.tex b/Acronyms.tex
index baf148c..dee41d4 100644
--- a/Acronyms.tex
+++ b/Acronyms.tex
@@ -9,4 +9,5 @@
     \acro{PEAS}{Performance, Environment, Actuators, Sensors}
     \acro{TSP}{Traveling Salesman Problem}
     \acro{CSP}{Constraint Satisfaction Problem}
+    \acro{KNF}{Konjunktive Normalform}
 \end{acronym}
\ No newline at end of file
diff --git a/chapters/Logik/Beweisverfahren.tex b/chapters/Logik/Beweisverfahren.tex
new file mode 100644
index 0000000..5b26052
--- /dev/null
+++ b/chapters/Logik/Beweisverfahren.tex
@@ -0,0 +1,51 @@
+\chapter{Beweisverfahren}
+\label{logik: beweisverfahren}
+    \section{Logische Folgerung}
+    \label{logische folgerung}
+        $$\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)$$
+        \includegraphics[width = .8\textwidth]{folgerung.png}\\
+        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}
+           \includegraphics[width = .8\textwidth]{inferenzregeln.png} 
+
+        \subsection{Beweis durch Resolution}
+        \label{beweis durch resolution}
+            $$\frac{A\vee B, \neg B\vee C}{A\vee C}$$
+
+        \subsection{Allgemeine Resolutionsregel}
+        \label{allgemeine resolutionsregel}
+            $$\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)}$$
+
+        \subsection{Klauselform}
+        \label{klauselform}
+            Die Klauselform ist die Mengendarstellung der \ac{KNF}:\\
+            \includegraphics[width = \textwidth]{klauselform.png}
+
+        \subsection{Resolutionsalgorithmus}
+        \label{resolutionsalgorithmus}
+            \includegraphics[width = .8\textwidth]{resolutionsalgorithmus1.png}\\
+            \includegraphics[width = .3\textwidth]{resolutionsalgorithmus2.png}
\ No newline at end of file
diff --git a/images/folgerung.png b/images/folgerung.png
new file mode 100644
index 0000000..a0b03a9
Binary files /dev/null and b/images/folgerung.png differ
diff --git a/images/inferenzalgorithmen.png b/images/inferenzalgorithmen.png
new file mode 100644
index 0000000..8d1b6ec
Binary files /dev/null and b/images/inferenzalgorithmen.png differ
diff --git a/images/inferenzregeln.png b/images/inferenzregeln.png
new file mode 100644
index 0000000..e7e1aaf
Binary files /dev/null and b/images/inferenzregeln.png differ
diff --git a/images/klauselform.png b/images/klauselform.png
new file mode 100644
index 0000000..133e15f
Binary files /dev/null and b/images/klauselform.png differ
diff --git a/images/resolutionsalgorithmus1.png b/images/resolutionsalgorithmus1.png
new file mode 100644
index 0000000..c92225f
Binary files /dev/null and b/images/resolutionsalgorithmus1.png differ
diff --git a/images/resolutionsalgorithmus2.png b/images/resolutionsalgorithmus2.png
new file mode 100644
index 0000000..d3a0a4b
Binary files /dev/null and b/images/resolutionsalgorithmus2.png differ
diff --git a/parts/Logik.tex b/parts/Logik.tex
index a7c58c9..5818030 100644
--- a/parts/Logik.tex
+++ b/parts/Logik.tex
@@ -3,4 +3,5 @@
 \input{chapters/Logik/Einführung.tex}
 \input{chapters/Logik/Formen der Inferenz.tex}
 \input{chapters/Logik/Logische Systeme.tex}
-\input{chapters/Logik/Aussagenlogik.tex}
\ No newline at end of file
+\input{chapters/Logik/Aussagenlogik.tex}
+\input{chapters/Logik/Beweisverfahren.tex}
\ No newline at end of file