Fragen zu Aufgabe 4 Probeklausur 1617

Bachelor Grundlagen der Logik in der Informatik
1

Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.

2

Fragen zu Aufgabe 4 Probeklausur 1617
Meine Frage ist ob ich bei der a tatsächlich den Schritt des negierens auslasse um zur Pränexform zu kommen oder ob ich den trotzdem mache?

Danke schonmal

3

In der Aufgabenstellung steht:

D.h. du sollst eine Formel in pränexe Normalform bringen, das ist alles. Und „der Schritt des negierens“ ist übrigens kein Teilschritt um zur Pränexform zu kommen!

4

Hat jemand dazu vllt mal seine Lösung? Damit man etwas vergleichen kann?:slight_smile:

5

Dann fange ich mal an: Erstmal allgemein, um die Gülltigkeit einer Formel allgemein zu beweisen, muss man die Formel negieren und den resolutionsalg. anwenden.
Bei Prädikatenlogik kann dieser Algorithmus ins Leere führen, da das Gültigkeitsproblem in der Prädikatenlogik nicht entscheidbar ist.
In der ersten Aufgabe soll man nur die Formel in Skolem bringen, d.h es hat nichts mit Gültigkeitsbeweis zu tun.

  1. ∀x((∀y(R(x, y)) ∨ ∃y(R(y, x))) → ∃z(S(x, z) ∧ S(z, x)))
  2. ∀x(-(∀y(R(x, y)) ∨ ∃y(R(y, x))) ∨ ∃z(S(x, z) ∧ S(z, x)))
  3. ∀x((∃y-(R(x, y)) ∧ ∀y-(R(y, x))) ∨ ∃z(S(x, z) ∧ S(z, x))) (NNF)
    Umbenennung der gebund. Variablen → d.h wir haben 2 unterschied. y ( y und y2)
  4. ∀x((∃y-(R(x, y)) ∧ ∀y2-(R(y2, x))) ∨ ∃z(S(x, z) ∧ S(z, x)))
  5. ∀x∃z∃y∀y2 (-(R(x, y)) ∧ -(R(y2, x))) ∨ (S(x, z) ∧ S(z, x))) (pränex)
  6. ∀x∃z∃y∀y2 ( (-R(x,y) ∨ S(x, z)) ∧ (-R(x,y) ∨ S(z, x)) ∧ (-R(y2,x) ∨ S(x, z)) ∧ (-R(y2,x) ∨ S(z, x)) (CNF)
  7. ∀x ∀y2 (-R(x,h(x)) ∨ S(x, f(x))) ∧ (-R(x,h(x)) ∨ S(f(x), x)) ∧ (-R(y2,x) ∨ S(x, f(x))) ∧ (-R(y2,x) ∨ [m][m][/m][/m]S(f(x), x)) (skolem)
  8. {-R(x,h(x)),S(x,f(x))} {-R(x,h(x)),S(f(x),x)} {-R(y2,x),S(x,f(x))} {-R(y2,x),S(f(x),x)}

Korrektheit ist nicht garantiert, wäre nett wenns jmd überprüfen könnte :wink:

6

Müsste man hier bei der Klauselmenge die Variablen auch umbenennen?

7

soweit ich weis ja :smiley: aber ich weis nicht zu welchem Teil die umbennung gehört.
Spätestens beim resolvieren muss man. Habs hier jetzt aber weggelassen.