From def82412221f391383acd9f74598e88ffc5b8aa8 Mon Sep 17 00:00:00 2001 From: paul-loedige Date: Mon, 8 Feb 2021 09:56:53 +0100 Subject: [PATCH] =?UTF-8?q?skolemisierungsverfahren=20hinzugef=C3=BCgt?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Readme.md | 2 +- chapters/Logik/Prädikatenlogik.tex | 12 ++++++++++++ 2 files changed, 13 insertions(+), 1 deletion(-) 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}