1. Если в формуле нет невыполнимых дизъюнктов, то выбираются l, S1 и S2, такие, что lÎ S1 и ù lÎ S2.
2. Строится резольвента r.
3. Заменяется S на SÈ{r}.
4. Процесс повторяется до порождения пустого дизъюнкта, это означает, что формула невыполнима.
Пример.Доказать невыполнимость следующего множества дизъюнктовS={pÚq, pÚr, ùqÚùr, ùp}.
Упорядочим множество S: S={pÚq, pÚr, ùqÚùr, ùp}.
1 2 3 4
Строим резольвенты для дизъюнктов, допускающих построение резольвенты:
5. (1, 3)® pÚùr;
6. (1, 4) ® q;
7. (2, 3)® pÚ ùq;
8. (2, 4)® r;
9. (2, 5)® p;
10. (4, 5)® ùr;
11. (4, 9)® F.
Замечания:
1. Если множество S не содержит ни одной пары дизъюнктов, допускающих резольвенту, то оно выполнимо.
2. Если выполнение алгоритма закончилось порождением пустого дизъюнкта, то установлена невыполнимость исходного S.
3. Может случиться, что выполнение алгоритма не завершится.
Применение метода резолюций означает построение соответствующего семантического дерева снизу вверх.