skolemisierungsverfahren hinzugefügt

chapters/Logik/Prädikatenlogik.tex

@@ -110,6 +110,18 @@
             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}