Seite 1 von 1

Aufgabe Resolution

Verfasst: 12. Sep 2016 10:55
von Smith
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?

Re: Aufgabe Resolution

Verfasst: 12. Sep 2016 13:48
von Alby407
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

Re: Aufgabe Resolution

Verfasst: 12. Sep 2016 14:46
von Smith
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 :)