5. Übungsblatt, G1

fetzer
Kernelcompilierer
Kernelcompilierer
Beiträge: 522
Registriert: 1. Okt 2008 17:18

5. Übungsblatt, G1

Beitrag von fetzer » 5. Sep 2010 20:32

Hi,

kleine Frage zur G1 vom 5. Übungsblatt. Dort wird in der MuLö die DNF für das Resolutionsverfahren genutzt, nicht die KNF.
Z.b. in i) für die erste Formel \((p \lor q) \rightarrow x\) müsste die Klauselmenge doch \(\lbrace \neg p, q, x\rbrace\) lauten und nicht \(\lbrace \lbrace \neg p,x \rbrace , \lbrace \neg q, x\rbrace \rbrace\) wie in der MuLö angegeben.

Falsch? Oder hab ich einfach was übersehen?

tobiwan
Mausschubser
Mausschubser
Beiträge: 75
Registriert: 15. Okt 2009 13:01
Wohnort: Langen

Re: 5. Übungsblatt, G1

Beitrag von tobiwan » 5. Sep 2010 22:42

Deins stimmt nicht ganz, da du die Implikation folgendermaßen auflösen musst:
Allgemein ist \(x \rightarrow y\) logisch äquivalent zu \(\neg x \lor y\)

Ergo hast du für \((p \lor q) \rightarrow x\) folgendes: \(\neg (p \lor q) \lor x\)

Also hast du dann \((\neg p \land \neg q) \lor x\)

JulM
Mausschubser
Mausschubser
Beiträge: 47
Registriert: 1. Okt 2009 19:25

Re: 5. Übungsblatt, G1

Beitrag von JulM » 5. Sep 2010 22:50

tobiwan hat geschrieben: Also hast du dann \((\neg p \land \neg q) \lor x\)
Was dann in KNF, wie folgt aussieht :
\((\neg p \lor x) \land ( \neg q \lor x )\)

Jetzt steht hier auch der komplette Weg ;)

fetzer
Kernelcompilierer
Kernelcompilierer
Beiträge: 522
Registriert: 1. Okt 2008 17:18

Re: 5. Übungsblatt, G1

Beitrag von fetzer » 5. Sep 2010 23:19

Autsch, ja natürlich.

Antworten

Zurück zu „Archiv“