diff --git a/Readme.md b/Readme.md index e235ae4..2babaa5 100644 --- a/Readme.md +++ b/Readme.md @@ -19,7 +19,7 @@ Dieses Repo beinhaltet die $\LaTeX$ Informationen für die Zusammenfassung im Fa - [x] Äquivalenztabelle aus Übung 5 (Aussagenlogik) - [x] Resolutionsalgorithmus (Hypothese wird negiert hinzugefügt) - [x] Äquivalenztabelle aus Übung 6 (Prädikatenlogik) -- [ ] Skolemisierungsverfahren hinzufügen +- [x] Skolemisierungsverfahren hinzufügen ## Hinweise Requires you to enable [--shell escape](https://tex.stackexchange.com/questions/516604/how-to-enable-shell-escape-or-write18-visual-studio-code-latex-workshop) diff --git a/chapters/Logik/Prädikatenlogik.tex b/chapters/Logik/Prädikatenlogik.tex index f8b35ce..3ec2259 100644 --- a/chapters/Logik/Prädikatenlogik.tex +++ b/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}