Resolution und Unerfüllbarkeit

Satz: Mod(F) = ∅$\iff$F $\vdash$ ∅      (in Worten: F in CNF nicht erfüllbar $\iff$ aus F kann man die leere Klausel ableiten.)

• Korrektheit ( ⇐): Übung.
• Vollständigkeit ( ⇒): Induktion nach | Var(F)|

dabei Induktionsschritt:

• betrachte F mit Variablen {x₁,…, x_n+1}.
• Konstruiere F₀ (bzw. F₁) aus F
  durch „Belegen von x_n+1 mit 0 (bzw. 1) ``

  (d. h. Streichen von Literalen und Klauseln)

• Zeige, daß F₀ und F₁ unerfüllbar sind.
• wende Induktionsannahme an: F₀ $\vdash$ ∅, F₁ $\vdash$ ∅
• kombiniere diese Ableitungen