Blatt 7, Aufgabe 2: Verbesserte Resolution

Bachelor Grundlagen der Logik in der Informatik
1

Konsistenz oder Erfüllbarkeit Zeigen?

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.

2

Blatt 7, Aufgabe 2: Verbesserte Resolution
Eigentliche Frage: Zeigt man mit Resolution nicht immer Erfüllbarkeit einer Formel? In der Aufgabe steht wir sollen zeigen, dass die CNFs konsistent sind. Dachte nur eine Formelmenge kann konsistent sein, keine einzelne Formel.

Bonusfragen:

  • Habe ich PLE soweit richtig verstanden, dass wenn ein Literal nur mit einer Polarität in allen Klauseln vorkommt, also z.B. A in {A,B},{C,not B},{not C, A}, ich alle Klauseln mit diesem Literal streichen kann. Ergebnis im Beispiel dann {C, not B}. Stimmt das? Käme not A in einer Klausel vor wäre hier keine PLE möglich.
  • Wenn ich einen Resolutionsschritt durchführe kommen ja letztendlich nur neue Klauseln hinzu. Heist das nicht, dass wenn am Anfang keine PLE möglich ist, sie später auch nicht möglich sein wird weil die Ursprünglichen Klauseln die PLE eventuell verhindern ja nie verschwinden?
3

Ja, mit der Resolution kannst du per se nur Erfüllbarkeit entscheiden.
Eine Formel ist gültig, wenn jede Belegung sie erfüllt. Das ist aber äquivalent dazu, dass ihre Negation unerfüllbar ist. Letzteres kannst du mit Resolution auch zeigen. Also kannst du mit Hilfe der Resolution auch Gültigkeit entscheiden.
(„entscheiden“ meine ich hier genau im Berechenbarkeitssinn. Dies gilt jedoch nur für die Aussagenlogik. Bei der Prädikatenlogik erster Stufe (FOL) kannst du Erfüllbarkeit nicht mehr entscheiden.)

Konsistenz einer Formelmenge ⇔ Es lässt sich aus der Formelmenge im betrachteten Kalkül (hier: Fitch mit (∨E), (¬E) usw.) kein Widerspruch herleiten.

In Aussagenlogik und FOL: Eine Formelmenge ist konsistent ⇔ sie erfüllbar ist.

  • Wenn du eine erfüllende Belegung für eine Formelmenge gefunden hast, so ist diese konsistent.
    Beweis: Sei Φ die Formelmenge und gelte κ ⊨ Φ. Angenommen, Φ wäre inkonsistent, also Φ ⊢ ⊥. Per Korrektheit der Aussagenlogik gilt: Φ ⊨ ⊥. Jedoch gilt für jede Wahrheitsbelegung κ ⊭ ⊥. Widerspruch.

  • Wenn eine Formelmenge konsistent ist, ist sie erfüllbar.
    Beweis: Per Kontraposition der Vollständigkeit der Aussagenlogik hast du Φ ⊬ ⊥ ⇒ Φ ⊭ ⊥. Wenn du die Definition von ⊨ auffaltest, siehst du, dass Φ ⊭ ⊥ äquivalent ist zu: es existiert eine Wahrheitsbelegung κ, sodass κ ⊨ Φ und κ ⊭ ⊥. Damit hast du Erfüllbarkeit.

(In FOL hast du keine Wahrheitsbelegungen, sondern, wie im Allgemeinen, Modelle. Es ändert sich aber nur die Notation, der Beweis nicht ;))

Eine einzelne Formel ist eine einelementige Formelmenge.

Genau, du hast es schon richtig verstanden :wink: Vielleicht hilft es, die Klauselmenge einmal nicht als Mengen abstrahiert zu sehen, sondern „roh“ in boolescher Algebra: [m](A ∨ B) ∧ (C ∨ ¬B) ∧ (¬C ∨ A)[/m]. Da A überall nur nichtnegiert vorkommt, kannst du ohne Beschränkung etwaiger Lösungsmengen (= erfüllende Belegungen) A als wahr in jeder erfüllenden Belegung annehmen. Damit sind die Klauseln, wo A vorkam, aber sowieso erfüllt und können gestrichen werden.

[quote=luisgerh]- Wenn ich einen Resolutionsschritt durchführe kommen ja letztendlich nur neue Klauseln hinzu. Heißt das nicht, dass wenn am Anfang keine PLE möglich ist, sie später auch nicht möglich sein wird weil die Ursprünglichen Klauseln die PLE eventuell verhindern ja nie verschwinden?
[/quote]
Durch PLE anderer Variablen oder Unit Propagation können diese Klauseln durchaus verschwinden.

Siehe auch DPLL algorithm - Wikipedia.

2 „Gefällt mir“