Negierte Klauselform

jojo1704
DON'T PANIC
Beiträge: 42
Registriert: 12. Apr 2011 11:18

Negierte Klauselform

Beitrag von jojo1704 » 15. Aug 2011 11:20

Hallo,

wir sitzen gerade an einer Aufgabe in der es darum geht eine Formel in Klauselform umzuwandeln.
Die Formel ist:

phi := ( q ^ r ) v not ( p v q v r )

Unsere Lösung ist:

not [ (not q v not r ) ^ ( p v q v r ) ]

Die Frage ist: Kann eine Klauselform auch komplett negiert sein oder gibt es eine andere Möglichkeit?

Jojo

Benutzeravatar
Domac
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 160
Registriert: 4. Okt 2010 16:11

Re: Negierte Klauselform

Beitrag von Domac » 15. Aug 2011 11:27

Bei welcher Aufgabe seid ihr denn?
Grundlegend sollte das kein Problem sein... aber erstmal die komplette Aufgabe bitte.
Extend my dropbox space (here).
Thanks!

jojo1704
DON'T PANIC
Beiträge: 42
Registriert: 12. Apr 2011 11:18

Re: Negierte Klauselform

Beitrag von jojo1704 » 15. Aug 2011 11:31

Die Aufgabe lautet:

Seien
phi := ( q ^ r ) v not ( p v q v r ) und psi := [not p ^ (r -> q)] v ( p ^ q ^ r)
aussagenlogische Formeln. Bringen Sie phi und not psi in Klauselform.

Wie schreibe ich denn das negierte dann in der Mengenschreibweise?
not { {not q , not r } , { p , q , r } } ?
Daraufhin soll man das Resolutionskalkül darauf anwenden. Nur wie mache ich das wenn die komplette Menge negiert ist?

Benutzeravatar
Domac
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 160
Registriert: 4. Okt 2010 16:11

Re: Negierte Klauselform

Beitrag von Domac » 15. Aug 2011 12:05

Also, man soll \(\varphi := (q \wedge r) \vee \neg(p \vee q \vee r)\) und \(\psi := (\neg p \wedge (r \rightarrow q)) \vee (p \wedge q \wedge r)\) zuerst in Klauselform bringen und dann das Resolutionskalkül darauf anwenden.
FGdI2 AL Skript hat geschrieben:Der Resolutionskalkül ist ein Kalkül, der auf den Nachweis der Unerfüllbarkeit von
AL-Formeln in KNF gerichtet ist. (Widerlegung/Refutation: Ableitungen im Resolutionskalkül sind formale, syntaktische Beweise für die Unerfüllbarkeit.)
Schreibe man jetzt \(\varphi \; als \; \neg \varphi\), dann erhält man \(\neg \varphi := \neg(q \wedge r) \wedge (p \vee q \vee r))\).
Man erhält für das Resolutionskalkül von \(\varphi \models \psi \equiv (\neg \varphi \wedge \psi)\).
Klauseln für \(\varphi\) sind also \(\{ \{\neg q, \neg r\}, \{p, q, r\} \}\).

Psi solltet ihr selbst hinkriegen und der Rest erschließt sich einem dann ja. Ich hoffe, dass da jetzt kein Denkfehler drinne ist. ^^
Gruß domac
Extend my dropbox space (here).
Thanks!

jojo1704
DON'T PANIC
Beiträge: 42
Registriert: 12. Apr 2011 11:18

Re: Negierte Klauselform

Beitrag von jojo1704 » 15. Aug 2011 12:18

Ich glaube du hast einen fehler, weil laut Lösung der Übung 9 ist \(\varphi \models \psi \equiv (\varphi \wedge \neg \psi)\).
Das Problem ist auch nur, dass wir nicht wissen wie man eine negierte Klauselform darstellen soll oder ob es die überhaupt gibt.

Benutzeravatar
Domac
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 160
Registriert: 4. Okt 2010 16:11

Re: Negierte Klauselform

Beitrag von Domac » 15. Aug 2011 12:25

Jup sorry. Einen kleinen Fehler hatte ich noch drinnen. Laut Skript ist \(\varphi \rightarrow \psi\) definiert als \(\neg \varphi \vee \psi\). Nun soll das Resolutionskalkül angewandt werden, welches Unerfüllbarkeit zeigt, also \(\neg (\varphi \models \psi) \equiv \models \neg (\varphi \rightarrow \psi)\) und daraus folgt ja \(\neg (\neg \varphi \vee \psi)\), also \(\varphi \wedge \neg \psi\).
So sollte es tun.

Gruß Domac

EDIT: Die Definition der Implikation ist aus dem AL Skript (ziemlich am Anfang). (Noch ein Fehler gefixt.)
Extend my dropbox space (here).
Thanks!

Antworten

Zurück zu „Archiv“