Kann so etwas ähnliches in der Klausur drankommen ?
Ich blick bei der Musterlösung nämlich überhaupt nicht durch!

Ich verstehs auch nicht -> hier wäre ein Walktrough sehr hilfreich.

Ich weiss dass das sehr viel Arbeit bedeutet, aber ich wäre auch sehr dankbar [img]http://www.fb18.de/gfx/15.gif[/img]

das sind an sich nur ein paar denkaufgaben zur resolution, die das ganze etwas klarer machen sollen… (alle angaben wie immer ohne gewähr)



wir wollen aus einer klauselmenge M eine kleinere, äquivalente klauselmenge M' finden - das heisst, wir suchen alles, was in M "unnütz" is und haun es raus…

a) Wenn wir nun zB eine Klausel K' haben, die Teilmenge von K ist (zB K' = {-A,B} und K = {-A,B,-C,D,E} oder so), dann können wir uns überlegen, dass wir alles, was wir mit K resolvieren könnten, auch mit K' resolvieren können

- Für den Fall, dass wir mit K herausbekommen würden, dass die Formel erfüllbar ist, wären irgendwo in den anderen Klauseln noch C,-D und -E. Wenn wir die nun also raushaun (K wegschmeissen und K' benutzen) könnten wir ganz normal weiter resolvieren und würden irgendwann an dem Punkt landen, wo wir keine weiteren Resolventen mehr bilden könnten
–> Also ist die Klauselmenge auch ohne -C, D und E resolvierbar und somit in diesem einen Fall äquivalent zur vorherigen

- Für den Fall, dass wir mit K feststellen, dass die Formel unerfüllbar ist (resolvieren bis zur leeren Klausel), würde das entweder heissen, wir haben -C, D und E einfach nicht benutzt und sind auch so bei der leeren Klausel gelandet (dann können wir sie ohne frage raushaun), oder aber, dass wir mit ihnen resolviert haben.
Wenn wir nun die größere der beiden Klauseln löschen, muss die kleine Klausel auf jeden Fall auch löschbar sein, denn sie war ja vollständig in der größeren enthalten und die konnten wir löschen

[edited] denkfehler behoben

wir wollen aus einer klauselmenge M eine kleinere, äquivalente klauselmenge M' finden - das heisst, wir suchen alles, was in M "unnütz" is und haun es raus…

a) Wenn wir nun zB eine Klausel K' haben, die Teilmenge von K ist (zB K' = {-A,B} und K = {-A,B,-C,D,E} oder so), dann können wir uns überlegen, dass wir alles, was wir mit K resolvieren könnten, auch mit K' resolvieren können

-> muss also K` schon in der Klauselmenge vorhanden sein oder bilden wir das selbst?

Ich hab aber ein Beispiel gefunden, bei dem das nicht klappt, denke ich:
K = {-A,C,E,-F}, K' = {-A,C}, K1 = {-E}, K2 = {F}.
Wenn wir nun K raushaun, is das Ding doch erfüllbar, oder?

Und wenn wir K drinne lassen ist es auch erfüllbar -> wo ist hier das Problem?

Also entweder is dasn Fehler in der MuLö oder ich steh grad mächtig neben mir… Muss evtl sogar die kleinere Menge anstelle der größeren gelöscht werden?

Es wird sehr verwirrend… …trotzdem danke, wenigstens einer der sich die Mühe macht..

K' und K müssen schon enthalten sein.
Wir betrachten uns einfach diejenigen Sonderfälle, in denen wir Klauseln verändern oder löschen können, weil sie in der Klauselmenge überflüssig sind, und in diesem Fall a) sind das die Klauseln, die vollständig in einer anderen enthalten sind