Vollständigkeit des Resolutionskalküls

#Studium #Informatik #Logik #Definition

Die Vollständigkeit besagt, dass der Kalkül stark genug ist, um alle unerfüllbaren Klauselmengen zu erkennen. Jede unerfüllbare Klauselmenge $C$ besitzt eine Resolutionswiderlegung ( $C$ ist unerfüllbar $\Rightarrow C ⊢_{R} ◻$ ).

Lemma (Vollständigkeit im Endlichen)

Jede unerfüllbare endliche Klauselmenge C hat eine Resolutionswiderlegung.

Beweisskizze (wie auf den Folien)

Induktion über die Anzahl der Variablen.
Zerlege $C$ nach einer Variablen $V_{n}$ in:
$C^{+}$ : Klauseln ohne $V_{n}$ , aus $C$ gewonnen durch Entfernen von $\neg V_{n}$ .
$C^{-}$ : Klauseln ohne $\neg V_{n}$ , aus $C$ gewonnen durch Entfernen von $V_{n}$ .
Zeige: Sind beide erfüllbar, erhält man ein Modell für $C$ (Widerspruch zur Unerfüllbarkeit).
Also sind $C^{+}$ und $C^{-}$ unerfüllbar; nach Induktionsvoraussetzung haben beide Resolutionswiderlegungen.
Kombiniere beide Widerlegungen plus einen letzten Resolutionsschritt zwischen ${\neg V_{n}}$ und ${V_{n}}$ zu einer Widerlegung von $C$ .