Beispiel für das Resolutionsverfahren
Beweise mittels Resolutionsverfahren, dass die Formel (in Klausel-Normalform)
$$ \langle [a],[\neg{b}],[\neg{a},b,c],[\neg{a},\neg{c}] \rangle $$
unerfüllbar ist.
1
$$ [a] $$
2
$$ [\neg{b}] $$
3
$$ [\neg{a},b,c] $$
4
$$ [\neg{a}, \neg{c}] $$
5
$$ [\neg{c}] $$
res(1,4)
6
$$ [\neg{a},c] $$
res(2,3)
7
$$ [\neg{a}] $$
res(5,6)
8
$$ [] $$
res(1,7)
Das Resolutionsverfahren im Beispiel. Zunächst werden die einzelnen Klauseln zeilenweise aufgeschrieben. Mittels Ableitung werden neue Klauseln erzeugt;
res(a,b) bezeichnet dabei die beiden Zeilen, aus welchen die Resolvente gebildet wurde (im aktuellen Schritt grün hinterlegt).