Aufgabe Resolution

Smith
Mausschubser
Mausschubser
Beiträge: 53
Registriert: 13. Apr 2015 15:45

Aufgabe Resolution

Beitrag von Smith » 12. Sep 2016 10:55

Hallo zusammen,

in der Lösung zu folgender Aufgabe wird die Folgebeziehung
A:= (p v ~q v r) & (~p v q v r) |= (~p & q & r) v (~p & ~q) v (~p -> 0)
gezeigt, indem per Resolution aus
B:= (p v ~q v r) & (~p v q v r) & (~p & q & r) v ((~p & ~q) v p)
die leere Klausel abgeleitet wird.

Ich verstehe nicht ganz wieso man das so macht.
Es geht nicht um den Schritt (~p & ~q) v (~p -> 0) <=> ((~p & ~q) v p),
sondern darum wie die Unverfüllbarkeit von B (also der selben Formel mit einem & anstatt einem |=) die Gültigkeit der Folgerungsbeziehung A zeigen soll.

Kann mir da jemand auf die Sprünge helfen?
Phil

Alby407
Mausschubser
Mausschubser
Beiträge: 64
Registriert: 19. Jul 2014 15:40

Re: Aufgabe Resolution

Beitrag von Alby407 » 12. Sep 2016 13:48

Hey! :)

Ganz allgemein kann man sagen, dass \(\varphi \models \psi\) genau dann, wenn \(\varphi \wedge \neg \psi \models\). (für zwei Formeln \(\varphi\) und \(\psi\)).
Und das ist eigentlich der ganze Zauber. In der Aufgabe wird die Folgerungsbeziehung so "umgeformt", dass man die Unerfüllbarkeit von \(\varphi \wedge \neg \psi\) beweisen muss. Und das können wir mit dem Resolutionskalkül bewerkstelligen, wenn wir mithilfe unseres Algorithmus die leere Klausel ableiten kann.

Du hast bei dir einen kleinen Fehler bei der Formel B. Hier muss nach dem & die Formel negiert werden.

Ich hoffe es ist verständlicher geworden :)

LG

Smith
Mausschubser
Mausschubser
Beiträge: 53
Registriert: 13. Apr 2015 15:45

Re: Aufgabe Resolution

Beitrag von Smith » 12. Sep 2016 14:46

Yeah, danke!
Stimmt, durch den Fehler mit der vergessenen Negierung hat das logisch keinen Sinn gemacht.
So kann ich gut nachvollziehen, dass wenn Y eine logische Folgerung aus X sein soll,
auch gelten muss, dass es nicht sein kann, dass X & ~Y erfüllbar ist.
Danke für's gute Erklären :)
Phil

Antworten

Zurück zu „Archiv“