die Formel (Klauselmenge) ist nicht erfüllbar
die leere Klausel ist durch Resolution ableitbar.
Beweispläne:
⇒ :
Gegeben ist die nicht erfüllbare Formel. Gesucht ist eine Ableitung
für die leere Klausel. Methode: Induktion nach Anzahl der
in der Formel vorkommenden Variablen.
⇐ : Gegeben ist die Ableitung der leeren Klausel.
Zu zeigen ist die Nichterfüllbarkeit der Formel.
Methode: Induktion nach Höhe des Ableitungsbaumes.
die leere Klausel ist durch Resolution ableitbar.