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.
Resolution
Wenn man beispielsweise die Folgenden zwei Klauseln vereinfachen wollen würde: {B; -C} und {C;-B;A} darf man da theoretisch doppelt vereinfachen sodass am Ende nur {A} rauskommt?? Oder ist das nicht erlaubt??
Schon mal danke für die Hilfe!!! 
Resolventen darf man nur bilden, wenn sich die beiden Klauseln in genau einem Literal unterscheiden. D.h. in diesem Fall ist es nicht erlaubt (würde zu einem falschen Ergebnis führen).
Einfaches Beispiel, warum das nicht geht: (A∨B)∧(¬A∨¬B), was der Klauselmenge {{A, B}, {¬A, ¬B}} entspricht, ist erfüllbar (wird z. B. von [A↦⊤, B↦⊥] erfüllt), wenn man jetzt aber A und B gleichzeitig eliminieren würde, würde man {{A, B}, {¬A, ¬B}, {}} bzw. (A∨B)∧(¬A∨¬B)∧⊥ herausbekommen, was offensichtlich nicht erfüllbar ist.
Bei der Resolution bin ich auch noch unsicher. Insbesondere wann man aufhören darf.
-
In einem Beitrag hier im Forum hat jemand die Resolution in Tabellenform aufgezeichnet. (Den entsprechenden Beitrag finde ich leider gerade nicht.) Tabellen gefallen mir deutlich besser als das Chaos mit den Pfeilen. Ist so eine Tabellenform auch gestattet in der Klausur?
-
Bei der Probeklausur SS12, Aufgabe 2 sieht für mich die KNF erfüllbar aus.
(A ∨ B ∨¬C) ∧ (A ∨ C ∨ B) ∧ (A ∨¬D) ∧ (B ∨ D) ∧ (¬A ∨ ¬B) ∧ (¬A ∨ B ∨ D) ∧ (¬D ∨ ¬A)
A B C D
-----------------------------------------
1 A B ¬C
2 A B C
3 ¬A B D
4 A ¬D
5 B D
6 ¬A ¬B
7 ¬A ¬D
-----------------------------------------
8 A B 1, 2
9 B ¬D 7, 8
10 B 5, 9
11 ¬A 6, 10
12 ¬D 4, 11
Muss man hier alle möglichen Terme erzeugen, um zu zeigen, dass die KNF erfüllbar ist?
Setzt man nach Zeile 12 [A↦⊥, B↦⊤, D↦⊥] sieht man ja, dass die Belegung von C sogar egal ist.
- Braindump WS12/13, Aufgabe 2
(D ∨ B ∨ ¬C) ∧ (D ∨ C) ∧ (¬D ∨ B) ∧ (¬C ∨ B ∨ ¬A) ∧ (C ∨ B ∨ ¬A) ∧ (¬B ∨ ¬A) ∧ (¬B ∨ A)
A B C D
-----------------------------------------
1 B ¬C D
2 ¬A B ¬C
3 ¬A B C
4 C D
5 B ¬D
6 ¬A ¬B
7 A ¬B
-----------------------------------------
8 ¬B 7, 8
9 ¬D 5, 8
10 C 4, 9
11 ¬A B 2, 3
12 ¬A 8, 11
13 ¬C D 1, 8
14 D 10, 13Hier kommt es zum Widerspruch zwischen Z. 9 und 14. Ist damit vollständig gezeigt, dass die KNF unerfüllbar ist?
Klauseln dürfen sich auch in mehr als einem Literal unterscheiden, insb. verschiedene Literale dürfen vorkommen - dann wird das Ergebnis aber dementsprechend lang.
{¬X,…}∪{¬D}, {X,…}∪{D} zu {¬X,X,…,…} in einer Klausel macht allerdings wenig sinn, da immer erfüllt, daher lässt man die weg.
Vgl. Resolution (Logik) – Wikipedia
{}∪{¬D}, {}∪{D} kannst du zu {} ableiten, und die leere Klausel ist nicht erfüllbar, also ist die ganze Formel unerfüllbar.
Ich verstehe nicht ganz, wieso das hier immer mit einer Tabelle gemacht wird. Fast überall wird das mit so einem Resolutionsbaum gemacht. Bekommt man dabei die leere Klausel irgendwann raus, dann ist der Ausdruck unerfüllbar. Sonst ist er erfüllbar (wie in dem Beispiel).
{A,B,-C}, {A,C}, {-C, D}, {C, D}
\ / \ /
{A,B} {D}
\ /
{A,B,D}
Oder versteh ich da irgend etwas ganz falsch?
Ja, so habe ich das zumindest in Erinnerung.
[quote=MrDeathly]
Ich verstehe nicht ganz, wieso das hier immer mit einer Tabelle gemacht wird. Fast überall wird das mit so einem Resolutionsbaum gemacht. Bekommt man dabei die leere Klausel irgendwann raus, dann ist der Ausdruck unerfüllbar. Sonst ist er erfüllbar (wie in dem Beispiel).
{A,B,-C}, {A,C}, {-C, D}, {C, D}
\ / \ /
{A,B} {D}
\ /
{A,B,D}
Oder versteh ich da irgend etwas ganz falsch?
[/quote]Das ist noch nicht fertig. Du musst alle möglichen Klauseln bilden, dabei darfst du „alte“ Klauseln auch mehrfach verwenden … es kommt also noch {A, D} aus {A, C} und {¬C, D} dazu. Außerdem: {A, B, ¬C} und {C, D} würden {A, B, D} ergeben, müsstest du auch noch hinschreiben, weil nämlich der Schritt von {A, B} und {D} zu {A, B, D} falsch ist (ok, wenn (A∨B)∧D erfüllbar ist, dann auch (A∨B)∧D∧(A∨B∨D), die Aussage an sich ist also nicht falsch, aber das ist nunmal kein Resolutionsschritt) …
Ich frage mich auch vieviele Klauseln wir herleiten müssen?
Hab bei der Probeklausur versucht alle herzuleiten und dann nach über 10 neuen aufgegeben…
Soviele bis du die leere Menge erzeugen konntest oder keine neuen Klauseln mehr finden kannst.
Edit: in der Regel wirst du in der Klausur die leere Menge erzeugen müssen, da dies relativ fix geht. Muss aber nicht.
Dass man alle herleiten muss kommt mir suspekt vor. Hab jetzt schon ein paar mal gelesen, dass so ein Baum eindeutig zeigen kann, ob eine Klauselmenge erfüllbar ist oder nicht. 
Aber werds in der Klausur wohl auch dann lieber vollständig mit Tabelle machen.
So ist nunmal der Algorithmus: Mache solange Resolutionsschritte, bis du keine neuen Klauseln mehr bekommst oder auf die leere Klausel stößt. Der arbeitet bewiesenermaßen korrekt und wenn ihr stattdessen einfach meint „ooooch, ich hab jetzt viele, das wird schon reichen“, ist das eben nicht immer korrekt.
Wo siehst du da eigentlich einen Baum? Der gerichtete Graph mit Kanten „von dieser Klausel kam ich auf jene“ ist i. A. nicht einmal ein Wald, sondern nur ein DAG.
Da hat wohl wer in AuD aufgepasst. 
Ja aber stimmt schon, mein Beispiel sah jetzt nur aus wie n Baum, wenn man das Teil umdreht. Sorry.
Ja hab nochmal ins Skript geschaut und die Resolvente wir ja mit der Klauselmenge vereinigt, uns auf diese Menge muss man dann den Algo weiter anwenden. Dann ergibt das schonmal Sinn.
Also würde die Lösung für mein Beispiel so aussehen:
A, B, -C
A, C
-C, D
C, D
A, B
A, B, D
A, D
D
Da man ab jetzt keine weiteren Resolventen mehr bilden kann ist KNF erfüllbar.
Danke auf jeden Fall für die Klarstellung, wären unnötig verschenkte Punkte gewesen für die Aufgabe.
So ist die Lösung richtig, ja (wenn du noch dran schreibst, welche der vier unteren Klauseln woher kommen ((1,2),(1,4),(2,3),(3,4))).
Muss man beim Ausführen des Resolutionsalgorithmus beispielsweise bei { A, ¬B, C} und { A, B, ¬C} die Mengen {A, C, ¬C} und { A, B, ¬B} hinzufügen?
Nein, denn:
- du kannst aus 2 Mengen in einem Schritt nur eine Resolvente bilden und
- das funktioniert in deinem Fall nicht (siehe weiter oben!)
Aus {A,¬B,¬C} und {A,B,¬C} ließe sich zum Beispiel die Resolvente {A,¬C} bilden.
Das funktioniert schon. Du bildest ja nicht in einem Schritt zwei Resolventen sondern in zwei Schritten jeweils eine Resolvente.
An sich ist das also korrekt.
Aber eine Resolvente zu bilden, in der X und ¬X, also jeweils das Atom und die negierte Version, vorkommen, ist unnötig/überflüssig und wird daher weggelassen.
Das hat phi hier schon erwähnt:
Nach meinem Verständnis ist es durch das Weglassen von solchen Resolventen auch nicht möglich, dass man irgendwelche anderen Resolventen dadurch nicht bilden kann, die zur Vollständigkeit des Beweises, dass die KNF erfüllbar ist, fehlen.
Wir haben da heute vom Lehrstuhl als Antwort bekommen, dass man sie weglassen kann, man aber argumentieren muss warum das Verfahren dann noch zuverlässig ist.