Umwandlung Pränexe Normalform in Klauselmenge

Question

Frage:

Ich habe folgende Aufgaben bearbeiten müssen:

Aufgabe 1 (Pränexe Normalform, Umwandlung in Klauselmenge). Überführen Sie die Formel \( F: \equiv \) \( \forall x . \exists y .(\forall z .(P(y) \rightarrow Q(x, z) \wedge Q(y, x)) \vee \exists z . \forall x .(Q(z, y) \rightarrow P(x))) \) schrittweise in eine Formel \( F^{\prime} \) in pränexer Normalform, die zu \( F \) äquivalent ist.

Aufgabe 2 (Pränexe Normalform, Umwandlung in Klauselmenge). Geben Sie zu der folgenden Formel eine erfüllungsäquivalente Klauselmenge an:
\(G:=\forall x . \exists y . \exists z . \forall v .((P(y, v) \vee Q(x) \rightarrow Q(y)) \wedge(Q(z) \rightarrow P(x, y)))\)

Meine Lösungsansätze wären folgende nur leider sind die laut Bewertung falsch:

1)

Um die Formel F in eine pränexe Normalform zu überführen, die zu F äquivalent ist, kann man die folgenden Schritte durchführen:
Skolemisieren: Ersetzen Sie jeden existentiellen Quantor durch eine Skolem-Funktion. In diesem Fall wird y durch f(x) ersetzt. F :≡∀x. ∃y. (∀z.(P(y) → Q(x, z) ∧ Q(y, x))∨ ∃z. ∀x.(Q(z, y) → P(x))) => F':≡∀x. (∀z.(P(f(x)) → Q(x, z) ∧ Q(f(x), x))∨ ∃z. ∀x.(Q(z, f(x)) → P(x)))
Negan: Negieren die Formel und bringen sie in die konjunktive Normalform F':≡∀x. (∀z.(P(f(x)) → Q(x, z) ∧ Q(f(x), x))∨ ∃z. ∀x.(Q(z, f(x)) → P(x))) => F'':≡∀x. ( (¬∀z.(P(f(x)) → Q(x, z) ∧ Q(f(x), x)) ∧ ¬(∃z. ∀x.(Q(z, f(x)) → P(x))))
Distribuieren der Negation über die Konjunktion F'':≡∀x. ( (¬∀z.(P(f(x)) → Q(x, z) ∧ Q(f(x), x)) ∧ (∃z. ¬∀x.(Q(z, f(x)) → P(x)))) =>F''':≡∀x. ( (∃z. ¬(P(f(x)) → Q(x, z) ∧ Q(f(x), x)) ∧ (∃z. ∃x. ¬(Q(z, f(x)) → P(x))))

Eliminieren der Implikation und der Konjunktion F''':≡∀x. ( (∃z. (¬P(f(x)) ∨ ¬Q(x, z) ∨ ¬Q(f(x), x)) ∧ (∃z. ∃x. Q(z, f(x)) ∧ ¬P(x))) =>F'''':≡∀x. ( (∃z. (¬P(f(x)) ∨ ¬Q(x, z) ∨ ¬Q(f(x), x)) ∧ (∃z. ∃x. (Q(z, f(x)) ∧ ¬P(x))))
Umwandeln in Klauselmenge F'''':≡∀x. ( (∃z. (¬P(f(x)) ∨ ¬Q(x, z) ∨ ¬Q(f(x), x))
2)
{ ¬P(y, v) ∨ ¬Q(x) ∨ Q(y), ∀x, ∃y, ∃z, ∀v ¬Q(z) ∨ P(x, y), ∀x, ∃y, ∃z Q(y) ∨ ¬Q(x) ∨ ¬P(y, v), ∀x, ∃y, ∃z, ∀v Q(y) ∨ P(x, y) ∨ ¬Q(z), ∀x, ∃y, ∃z }

Kann mir hier vielleicht jemand erklären wo meine Fehler sind und mir einen korrekten Lösungsweg geben? Ich wäre dafür sehr dankbar, da ich hier nicht weiter komme und die Aufgabe vorstellen soll/muss

Answer 1

Aufgabe 1. Formeln in pränexer Normalform dürfen Existenzquantoren enthalten. Skolemisierung ist deshalb nicht notwendig.

Es dürfen keine zwei Quantoren die gleiche Variable quantifizieren. Außerdem darf keine Variable sowohl frei als auch gebunden vorkommen. Entsprechende Variablen müssen umbenannt werden. Die so erhaltene Form heißt bereinigt. Aus

    \( \forall x . \exists y .(\forall z .(P(y) \rightarrow Q(x, z) \wedge Q(y, x)) \vee \exists z . \forall x .(Q(z, y) \rightarrow P(x))) \)

wird somit

    \( \forall x . \exists y .(\forall z .(P(y) \rightarrow Q(x, z) \wedge Q(y, x)) \vee \exists z' . \forall x' .(Q(z', y) \rightarrow P(x'))) \).

Jetzt können die Quantoren einfach nach vorne geholt werden:

    \( \forall x . \exists y .\forall z .\exists z' . \forall x'.((P(y) \rightarrow Q(x, z) \wedge Q(y, x)) \vee (Q(z', y) \rightarrow P(x'))) \).

Aufgabe 2. Zur Umwandlung einer Formel in eine erfüllungsäquivalente Klauselmenge wird die Formel zunächst in pränexe Normalform gebracht. Das erübrigt sich bei \(G\), weil \(G\) bereits in pränexer Normalform vorliegt.

Jetzt skolemisieren, das heißt die Existenzquantoren wegwerfen und die Variablen \(y\) und \(z\) ersetzen durch Funktionssymbole \(y(x)\) bzw \(z(x)\) ersetzen. Dann hast du

    \(\forall x . \forall v .((P(y(x), v) \vee Q(x) \rightarrow Q(y(x))) \wedge(Q(z(x)) \rightarrow P(x, y(x))))\).

Dann den quantorenfreien Teil

    \((P(y(x), v) \vee Q(x) \rightarrow Q(y(x))) \wedge(Q(z(x)) \rightarrow P(x, y(x)))\)

nach den Regeln der Aussagenlogik in konjunktive Normalform überführen und die Konjunktionen jeweils in Mengenschreibweise zusammenfassen.