Beleg der Erfüllbarkeit mittels Resolutionsverfahren
Das Resolutionsverfahren lässt sich nicht nur nutzen, um die Allgemeingültigkeit einer Formel nachzuweisen, sondern auch, um zu belegen, dass dies eben nicht der Fall ist. Das bedeutet, dass
mittels Resolution in endlicher Zeit alle möglichen Resolutionsableitungen einer gegebenen Formel gebildet werden können. Besteht keine dieser Ableitungen aus einer leeren Klausel
(bzw. eine Resolutionswiederlegung) bedeutet dies, dass die Negation ¬ F der Formel F erfüllbar ist.
F ist damit wiederlegbar und nicht allgemeingültig.
Durch diese Eigenschaft stellt die Resolution ein Entscheidungsverfahren dar.
Nachfolgend wird an einem Beispiel die Erfüllbarkeit einer Formel mittels Resolution illustriert.
Beweise mittels Resolutionsverfahren, dass die Formel (in Klausel-Normalform)
$$ \langle [\neg{a},b,\neg{c}],[\neg{a},b,d],[a,b],[b,c],[b,\neg{d}] \rangle $$
erfüllbar ist.