Lsg. Ansatz zur Altklausur Aufgabe 4 von WS1617

Lsg. Ansatz zur Altklausur Aufgabe 4 von WS1617

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.

Lsg. Ansatz zur Altklausur Aufgabe 4 von WS1617
https://www.dropbox.com/s/dm2anh1rsufk4u0/1.jpg?dl=0,
https://www.dropbox.com/s/bpv5g4wksx7hrvk/2.jpg?dl=0
kann jemand ueberpruefen, ob es stimmt?


y,z müssten durch einstellige von Funktionen mit Parameter x ersetzt werden, da \forall x vor \exists y,z steht.

Bei anderer Reihenfolge: Erste ex. dann all. Quantoren hättest du anstelle der Funktionen, Konstanten für die jeweiligen Variablen.


Bitte die Dateien im Forum hochladen um zu gewährleisten, dass sie nicht gelöscht werden und immer verfúgbar sind.


https://www.dropbox.com/s/7dicdecgtpo20wv/11.jpg?dl=0
https://www.dropbox.com/s/5j043acgookf36j/12.jpg?dl=0
[color=crimson]ich habe eine Frage zur b) die Resolution, wenn ich zum Ende Q(x)= nicht Q(a) bekommen, dann habe x=a , a als konstanten ,kann
x einsetzen , zum Ende bekomme ich noch nicht p(f(a)), damit ist unerfüllbar , dann ist die “richtige Formel” gültig so?![/color]


das problem ist , ich weiße nicht, wie ich die Datei in Forum speichern!!! :-/


  1. Momo, du kannst in den “Post Options” sagen, dass du eine Datei hochladen möchtest und kannst dann eine Datei auswählen.

  2. Zu b): Habe ich sehr ähnlich, siehe Anhang.

Attachment:
Aufgabe 4b - Resolution - 4.4.17.pdf: https://fsi.cs.fau.de/unb-attachments/post_152440/Aufgabe 4b - Resolution - 4.4.17.pdf


Zur b)
Ist es nicht verboten Funktionen durch Konstanten zu ersetzen? Also f(x) → a?

1 „Gefällt mir“

Ich habe nirgendwo gelesen, dass es gilt bzw. nicht gilt. Angenommen, es gelte, dann könnte man P(x) und \lnot P(f(x)) resulieren. Wenn man das dann aber konsequent durchziehen kann/darf, dann kann man vermutlich alles kaputt machen, was man möchte. Das wirkt auf mich jetzt nicht besonders praktikabel und somit vermutlich tatsächlich nicht einfach machbar.


Wenn es erlaubt wäre, dann könnte man mit den Probeklausur die Anfangsklauseln 3 {R(f(x),a)} und 4 {-R(c,a)} bereits die leere Klausel erreichen. Denk daher auch nicht, dass es so einfach geht.

Bei Momos 4b ist mir aufgefallen, dass Klausel 3 {-P(x), -S(x,y), Q(y)} lautet, in dem Braindump heißt die Klausel aber {-R(x,y), -S(x,y), Q(y)}. Damit ändert sich natürlich die Resolution. Kann aber auch nicht sagen, welche Version die richtige ist.


Das sind die einzigen Regeln, die Wikipedia angibt. Aber damit hab ich es schon oft probiert und komme auf keinen grünen Zweig.


ich habe so gelöst, aber eine Frage ist , wenn ich 6+7 Klausel zusammenführen, kann ich die beide noch übliche Klausel zusammen in einer Klausel führen?

ok


  1. R(x,f(x))
  2. P(f(x))
  3. -P(x),-s(x,y),Q(y)
  4. -R(x,y),-P(y),s(y,x)
  5. -Q(a)

1+4: R(x,f(x))=R(x,y) mgu=[f(x)/y]
6. -P(f(x)),s(f(x),x)
2+3: P(f(x))=P(x) mgu=[f(x)/x]
7. -s(f(x),y),Q(y)
6+7: s(f(x),x)=s(f(x),y)
mgu=[x/y]
8. -p(f(x),Q(x)
2+8: Q(x) 9
5+9: mgu=[a/x]
unerfüllbar


Konstanten darf man nicht ersetzten. In der Lösung wird auch keine Konstante ersetzt.

Variablen darf man beliebig ersetzten, egal durch was; auch durch Konstanten und andere Funktionssymbole. Deshalb ist die Substitution

x ↦ c
y ↦ d

auch erlaubt. Wenn etwas für alle x gilt, dann gilt es auch für die Konstante c. Andersherum dürfte man es natürlich nicht.
ss2016 Resolutionsverfahren was macht man mit konstante? - Grundlagen der Logik in der Informatik - FSI Informatik Forum kommentar von errbosys(Lehrstuhlmitarbeiter)


Laut dem Braindump https://fsi.cs.fau.de/git_public/braindumps/gloin/2017-04-04/gloin_2017-04-04_braindump.pdf ist die 4. Klausel anders. Hast du dir das in der letzten Klausur so aufgeschrieben und der Braindump ist falsch, oder hast du das nur falsch abgeschrieben und die Klauseln des Braindump sind korrekt?

  1. {R(x, f (x))}
  2. {P (f (x))}
  3. {¬R(x, y), ¬S(x, y), Q(y)}
  4. {¬R(x, y), ¬P (x), S(y, x)}
  5. {¬Q(a)}

Dein Lösungsweg sollte so passen, Trinram hat sich auf die Lösung von Ezekiel bezogen. Dort wird f(x) → a ersetzt.
Gerne würde ich glauben, dass deine Klauseln die richtigen sind, bei denen des Braindumps steck ich nämlich fest und komm einfach nicht zu einem sinnvollen Ergebnis.

Mögliche Klauseln:
6. 1+4 y->f(x): -P(x), S(f(x),x)
7. 2+4 x->f(x): -R(f(x), y), S(y, f(x)) (R verschwindet nicht da, man nicht über Kreuz substituiert)
8. 2+6 x->f(x): S(f(f(x)), f(x))
9. 1+3 y->f(x): -S(x, f(x)), Q(f(x)) (Q verschwindet nicht mehr, da f(x) <-/-> a)
10. 3+5 y->a : -R(x,a), -S(x, a) (R - " - )


ich habe den originale alte Klausur kopie!!! die briamdaump ist falsch!


ich habe den originale alte Klausur kopie!!! die briamdaump ist falsch!


habe ich meine Lösung zusammengefasst

  1. R(x,f(x)) 2. P(f(x)) 3. -P(x),-s(x,y),Q(y) 4. -R(x,y),-P(y),s(y,x) 5. -Q(a)

1+4: R(x,f(x))=R(x,y) mgu=[f(x)/y]
(6). -P(f(x)),s(f(x),x)

                          2+3:   P(f(x))=P(x) mgu=[f(x)/x]         
                         (7). -s(f(x),y),Q(y)
                   
            
                         5+7: Q(y)=Q(a)
                            mgu=[a/y]
                         (8) -s(f(x),a)

6+8: s(f(x),x)=s(f(x),a)
mgu=[a/x]
(9)-P(f(a))
9+2: mgu=[a/x]
unerfüllbar!!


Darf man die Variable durch eine Funktion mit derselben Variable ersetzen? also x → f(x)?