Zeigen Sie mit Hilfe der Resolution, dass die unten stehenden semantischen Folgerungen gelten:

Question

Guten Abend;

die Aufgabe ist folgende:

Aufgabe 2 (Resolution)
Zeigen Sie mit Hilfe der Resolution, dass die unten stehenden semantischen Folgerungen gelten:
a) \( \alpha \vDash(B \vee C) \) mit \( \alpha=(((A \vee B) \wedge(\neg A \vee C)) \vee(C \vee \neg D)) \wedge(C \vee D) \)
b) \( \beta \vDash \neg E \) mit \( \beta=(A \vee \neg B \vee \neg E) \wedge(B \vee \neg F \vee \neg E) \wedge(\neg E \vee \neg A) \wedge(\neg B \vee F \vee \neg A) \wedge(F \vee \neg E) \). Verwenden Sie eine Unit-Resolution.

Problem/Ansatz:

Zu a)

Mein Problem hierbei ist zu verstehen, wie ich genau vorgehen muss, dass gezeigt wird, dass auch dem Alpha (B "oder" C) folgt.

Wäre es richtig, wie bei der aussagenlogischen Resolution vorzugehen und wenn am Ende B "oder" C rauskommt, so habe ich das bewiesen?

zu b)

evtl komme ich da selber drauf, wenn ich verstanden habe was in a genau gemacht werden muss

Answer 1

a) Du musst Resolution benutzen. Entweder du zeigst, dass am Ende (B ∨ C) erzeugt werden kann, oder wahlweise, was auch viel einfacher ist, nimmst du die Negation von (B ∨ C) mit in deine Bedingung auf und zeigst, dass dies unerfüllbar ist.

Also \( \alpha \vDash(B \vee C) \) äquivalent zu ∝ ∧ ¬(B ∨ C) unerfüllbar. Das müsstest du dann noch in KNF bringen und dann Resolution anwenden.

b) Dasselbe wie bei a). Hier musst du aber die Negation von ¬E (also E) auf die andere Seite bringen, da du ansonsten nicht Unit Resolution anwenden kannst und dann zeigen, dass das unerfüllbar ist. Reminder: Unit Resolution ist die Resolution über ein einzelnes Literal innerhalb einer Klausel.

Also \( \beta \vDash \neg E \) äquivalent zu beta ∧ E unerfüllbar.