Korrektheit des Resolutionskalküls

#Studium #Informatik #Logik #Definition

Die Korrektheit besagt, dass der Kalkül keine falschen Schlüsse zieht. Wenn aus einer Klauselmenge $C$ die leere Klausel abgeleitet werden kann ( $C ⊢_{R} ◻$ ), dann ist die Klauselmenge $C$ auch tatsächlich unerfüllbar.

Lemma (Korrektheit)

Wenn $C ⊢_{R} D$ , dann $C ⊨ D$ .
Insbesondere: Wenn $C ⊢_{R} □$ , dann ist $C$ unerfüllbar.

Beweisskizze

Induktion über die Länge der Resolutionsableitung.
Basis: Startklauseln sind in $C$ , also triviale Konsequenzen.
Schritt: Neue Klausel entsteht per Resolution aus zwei früheren, ist wegen lokaler Korrektheit eine semantische Konsequenz dieser; mit Induktionsannahme damit auch Konsequenz von $C$ .