Resolution (Vollständigkeit)

die Formel (Klauselmenge) ist nicht erfüllbar $\iff$ mathend000# die leere Klausel ist durch Resolution ableitbar.

Bsp: {p, q,¬p∨¬q} mathend000#

Beweispläne:

• ⇒ mathend000# : 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.
• ⇐ mathend000# : Gegeben ist die Ableitung der leeren Klausel. Zu zeigen ist die Nichterfüllbarkeit der Formel. Methode: Induktion nach Höhe des Ableitungsbaumes.