FB18 - Das Forum für Informatik

fb18.de / Bachelorstudieng / PM Formale Informatik

aufgabe 7.4

aufgabe 7.4 2007-05-20 23:38
Anonymer User
kann mir jemand sagen was bei der aufgabe genau gemeint ist?

ist nicht der beweis des resolutionslemmas nicht schon der beweis für diese äquivalenz?

RE: aufgabe 7.4 2007-05-20 23:57
Wulf
Ich frag mich bei der Aufgabe eher, wie man so ein i und j wählen soll, wenn meine Klauselmenge z.B. { (A) , (B) } ist.
Wenn du einfach nur einen anderen Beweis 1:1 kopieren müsstest, wäre das zu einfach. Denk mal bisschen mehr darüber nach ;-)

RE: aufgabe 7.4 2007-05-21 00:09
matten
wenn deine Klauselmenge {{A},{B}} ist, so ist sie nicht nach Aufgabenstellung. Es soll ein i,j (1 <= i < j <= n) derart geben, dass sich die Formel F' aus F bilden lässt, indem man k_i und k_j aus F entfernt und in F als (k_i - {L}) u (k_j - {/L}) wieder einfügt. (k_i bezeichne die Klausel mit Index i).

allerdings legt das eine Kopie des Beweises vom Resolutionslemma nahe :/

RE: aufgabe 7.4 2007-05-21 00:33
Wulf
Ist trotzdem keine exakte, korrekte Formulierung. Bin gerade ein wenig paranoid was korrektes angeht, ich programmier nebenbei was mit Threads.

leicht OT: Bei mir ist F1 (F2?) schon paar Jahre her, Wikipedia hilft bei formaler Informatik ziemlich gut. Sogar zur Resolution gibt's einen brauchbaren Artikel *Zaunpfahl*

RE: aufgabe 7.4 2007-05-21 03:38
Goldl
ist nicht der beweis des resolutionslemmas nicht schon der beweis für diese äquivalenz?

Der Beweis ist nicht der Beweis für diese Äquivalenz. Ist aber ein guter Anhaltspunkt, was man für ein Gegenbeispiel nehmen könnte und wie man eine semantische Eigenschaft findet bzw. begründet.
wenn deine Klauselmenge {{A},{B}} ist, so ist sie nicht nach Aufgabenstellung

Eine ähnliche Klauselmenge die geht ist {K1,K2}
wobei gilt: L element K1
not L element K2

RE: aufgabe 7.4 2007-05-22 00:30
ole
man sollte sich zunächst einmal die mengen ganz genau ansehen.
anschließen die definition der resolventen menge.
dann sieht man recht schnell worum es eigentlich geht.