Resolution und Unerfüllbarkeit

Satz: F mathend000# in CNF nicht erfüllbar $\iff$ mathend000# es gibt eine Resolutions-Ableitung der leeren Klausel.

Beweis:

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

dabei Induktionsschritt:

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

  (d. h. Streichen von Literalen und Klauseln)

• Zeige, daß F₀ mathend000# und F₁ mathend000# unerfüllbar sind.
• wende Induktionsannahme an.