Wie an die Resolution rangehen?
Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.
Blatt 7, Aufgabe 4
Hallo zusammen!
Ich wollte gerade die Aufgabe 4 vom Blatt 7 bearbeiten ( (Dame v Tiger) ^ Resolution ).
https://www8.cs.fau.de/_media/ws14:gloin:uebung07.pdf
Aber irgendwie weiß ich nicht genau, wie ich rangehen soll. Außerdem hab ich noch nicht ganz verstanden, was mir das mit der Resolution überhaupt so bringen soll. Kann mir das jemand vielleicht weiterhelfen?
Also ich muss die aussagenlogische Form in eine CNF umwandeln, damit ich die Klauselmenge für das Resolutionsverfahren habe. Das ist soweit klar, denke ich. Aber wenn man das halbwegs sinnvoll umformt, dann bleiben kaum noch Klauseln übrig. Bzw. bei mir halt nur noch eine.
Und wenn ich das Resolutionsverfahren durchziehe: was sagt mir das “Ergebnis” dann?
Wäre dankbar, wenn da jemand bei mir Licht ins Dunkel bringen könnte 
Danke!
Hey,
Das Resolutionsverfahren ist ein (nicht det.) Algorithmus um herauszufinden ob eine CNF erfüllbar ist.
Der Algorithmus selbst ist relativ einfach und du kannst ihn im inoffiziellen Skript nachlesen.
Hier ein Beispiel:
Im Prinzip versuchst du die Klauseln in der Klauselmenge so lange zu kombinieren bis entweder die leere Menge herauskommt (symbolisiert durch Kasten) oder es keine weitere Möglichkeit mehr gibt die Klauseln zu kombinieren.
Wenn du die leere Menge bekommst ist die CNF nicht erfüllbar (nicht erfüllbar = falsch) Wenn es unmöglich ist die leere Menge zu erreichen, so ist die CNF erfüllbar( Im Beispiel ist die Formel also nicht erfüllbar.)
Diesen Algorithmus kann man auch verwenden um zu zeigen dass eine CNF wahr ist. Dazu nimmst du die Negation der CNF, wandelst diese wieder in eine CNF um und führst für diese den Resolutionsalgorithmus aus. Sollte die Negation nicht erfüllbar sein, so ist die eigentliche CNF immer erfüllbar (=wahr).
Ich hab selber die Aufgabe noch nicht gerechnet, aber ich denke du sollst die CNF nicht vereinfachen sondern direkt den Resolutionsalgorithmus verwenden.
Hoffe es hilft 
1 „Gefällt mir“