Seite 1 von 1

Übungsblatt 2 - Resolutionsverfahren

Verfasst: 23. Aug 2011 15:59
von fscheepy
Hallo,
ich wollte mal fragen, wie man mit dem Resolutionskalkül am besten zeigt, dass eine Formel erfüllbar ist, also dass man aus ihr nicht den "Kasten" ableiten kann. Auf dem Übungsblatt 2 (uebung09) kommt in der G2a ja eine entsprechende Aufgabe dran. Reicht es da nicht, direkt zu schreiben, dass man das ~r nicht eliminieren kann, da in der Formel gar kein r vorkommt? Und was hat es in der Musterlösung mit diesem rekursiven Aufzählen auf sich (Res0(K), Res1(K),...)? Ich hab das bisher immer so ähnlich gemacht wie in der Musterlösung der G2b: die Formel in eine Zeile aufgeschrieben, markiert, was ich rausschmeiße, die neue Formel in der nächsten Zeile aufgeschrieben usw...ich nehme an wir müssen nicht unbedingt dieses rekursive Aufzählen der Klauselmenge benutzen?

/edit: Noch eine weitere Frage: Kann man den Resolutionsalgorithmus nicht schon direkt abbrechen, wenn man in der Menge zwei Klauseln hat, die sich gegenseitig ausschließen (z.B. einmal (p v q) und einmal (~p v ~q)?

Re: Übungsblatt 2 - Resolutionsverfahren

Verfasst: 23. Aug 2011 19:40
von bafnai
Hallo,
ich habe noch zwei Ergänzungsfragen.

1. Zu Übungsblatt 2, G2, a)
Hier steht in der Lösung:

Res\(^0(K) = \{\{p, \neg q, \neg r\}, \{\neg p, q, \neg r\}, \{\neg p, \neg q\}\}\)
Res\(^1(K) =\\)Res\(^0(K)\cup \{\{q, \neg q, \neg r\}, \{\neg q, \neg r\}\{p, \neg p, \neg r\}, \{\neg p, \neg r\}\}\)
Res\(^2(K) =\\)Res\(^1(K)\cup \{\{\neg p, \neg q, \neg r\}\}\)
Res\(^3(K) =\\)Res\(^2(K)\)

Müsste bei Res\(^2(K)\) nicht auch noch \(\{q, \neg q, p, \neg p, \neg r\}\) (aus \(\{q, \neg q, \neg r\}\) und \(\{p, \neg p, \neg r\}\)) stehen, oder habe ich etwas falsch verstanden?

2. Allgemein zu den Ableitungsbäumen beim Resolutionsverfahren.
Gibt es ein System oder läuft es auf Ausprobieren hinaus?

MfG bafnai

Re: Übungsblatt 2 - Resolutionsverfahren

Verfasst: 23. Aug 2011 19:58
von dschneid
fscheepy hat geschrieben:Reicht es da nicht, direkt zu schreiben, dass man das ~r nicht eliminieren kann, da in der Formel gar kein r vorkommt?
Sicher, das wäre eine völlig ausreichende Begründung. Ansonsten ist die Resolution sehr schlecht geeignet, um Erfüllbarkeit zu zeigen. Man müsste, wie in der Musterlösung, alle Resolventen bilden und feststellen, dass die leere Klausel nicht darunter ist.
fscheepy hat geschrieben:Und was hat es in der Musterlösung mit diesem rekursiven Aufzählen auf sich (Res0(K), Res1(K),...)?
Da wird der Algorithmus durchgeführt, wie man ihn maschinell implementieren würde. In jedem Schritt werden alle Resolventen der schon vorliegenden Klauselmengen gebildet und für den nächsten Schritt hinzugefügt. Der Computer hat ja keine Intuition, welche Klauseln er am besten vereinigt, also muss er alle bilden und schauen, ob irgendwann die leere Klausel vorkommt. Als Mensch macht man das natürlich zielgerichtet mithilfe der Baumschreibweise (die du ja glaube ich meinst).
fscheepy hat geschrieben:Noch eine weitere Frage: Kann man den Resolutionsalgorithmus nicht schon direkt abbrechen, wenn man in der Menge zwei Klauseln hat, die sich gegenseitig ausschließen (z.B. einmal (p v q) und einmal (~p v ~q)?
Schon, aber das wäre nicht mehr wirklich die Idee des Resolutionskalküls, das ja gerade eine sehr mechanische und gleichförmige Methode liefert, so etwas zu testen. Kalküle sollen ja nur mit reiner Syntax arbeiten, aber wenn du überprüftst, ob zwei Klauseln unverträglich sind, dann gehst du wieder auf eine semantische Ebene. (In der Klausur ist natürlich im Zweifelsfall jedes Mittel recht, da ist allerdings auch so eine Aufgabe eher unwahrscheinlich).
bafnai hat geschrieben:Müsste bei Res\(^2(K)\) nicht auch noch \(\{q, \neg q, p, \neg p, \neg r\}\) (aus \(\{q, \neg q, \neg r\}\) und \(\{p, \neg p, \neg r\}\)) stehen, oder habe ich etwas falsch verstanden?
Ich habe es nicht überprüft, aber ich meine mich zu erinnern, dass ich in der Übung damals tatsächlich einen Fehler entdeckt hatte; das kann also sein.
bafnai hat geschrieben:Gibt es ein System oder läuft es auf Ausprobieren hinaus?
Das System (für AL jedenfalls) wäre es, alle Resolventen zu erzeugen, was aber in der Praxis natürlich Unsinn ist. Man macht also tatsächlich "educated guesses". Im Kern schaut man dabei, wie man jeweils ein Literal aus der Klausel loswerden kann, also wie man eine Klausel herleiten kann, die bis auf die Negierung des entsprechenden Literals gleich aussieht oder noch kürzer ist (wohingegen es eigentlich nie etwas bringt, mit Klauseln zu resolvieren, die andere Variablen haben). Deswegen sollte man möglichst auf eine gewisse Symmetrie der vorgegebenen Klauseln achten, dann findet man meistens recht schnell einen Weg.

Re: Übungsblatt 2 - Resolutionsverfahren

Verfasst: 24. Aug 2011 12:04
von hstr
bafnai hat geschrieben:Hallo,
ich habe noch zwei Ergänzungsfragen.

1. Zu Übungsblatt 2, G2, a)
Müsste bei Res\(^2(K)\) nicht auch noch \(\{q, \neg q, p, \neg p, \neg r\}\) (aus \(\{q, \neg q, \neg r\}\) und \(\{p, \neg p, \neg r\}\)) stehen, oder habe ich etwas falsch verstanden?
Ich glaube nicht, da die beiden Klauseln \(\{q, \neg q, \neg r\}\) und \(\{p, \neg p, \neg r\}\) keine Resolvente bilden. (Skript S.13 Def. 5.4)