Resolutionsmethode Aussagenlogik

Question

Habe bei folgender Aufgabe Schwierigkeiten:

Aufgabe:

Nutzen Sie die Resolutionsmethode um zu beweisen, dass die Menge K1 aussagenlogischer Klauseln nicht erflülbar ist.

 a) K1 = {{Z, Y }, {Z, X, ¬Y }, {¬Z, W}, {Z, ¬X, ¬Y }, {¬W}}

Problem/Ansatz:

Nicht erfüllbar heißt ja, am Ende soll eine Leere Menge dastehen. Verstehe jedoch die Resolution nicht und habe im Internet nichts gefunden was mir weiter geholfen hätte.

Answer 1

Bei der Resolution müssen ja alle möglichen Verschmelzungen von Klauseln mit komplementären Literalen gebildet werden. Da dies selbst in dem kleinen Beispiel schon sehr viele sind, lohnt sich allerdings vorheriges überlegen, was einen zum Ziel führt.

Bei der Resolution von (Z,X,¬Y) und (Z,¬X,¬Y) ist dir ein Fehler unterlaufen und was du im letzten Schritt gemacht hast, verstehe ich nicht, dort hast du doch gar keine komplementären Literale zu stehen.

Wenn du den erst genannten Fehler korrigierst solltest du aber auf die Klausel (¬Y) kommen. Wenn du dann nochmal auf die Anfangsklauseln schaust, solltest du einen Weg erkennen, wie du in zwei Resolutionsschritten zur Klausel (Y) kommst, was dir dann den gewünschten Widerspruch liefert.