Метод резолюций

Если имеются два высказывания: которые имеют контрарные или инверсные () литералы, то следствием из этих посылок является (BÚC). Проверим это утверждение:

Такие следствия называются резольвентами (это дизъюнкция членов при контрарных литералах).

Метод основан на получении резольвент. Последовательно получаем резольвенты исходного множества формул, доказательство невыполнимости которого мы ведем, до тех пор, пока не получится Æ (пустое следствие). Здесь доказательство ведется от противного.

Для применения этого метода необходимо использовать КНФ. Например, для modus ponens:

Получили дерево доказательства. Взяты две посылки и отрицание заключения в КНФ. Следствием посылок является резольвента B, а следствием является пустое множество Æ. Это признак невыполнимости исходного множества членов КНФ. А т.к. доказательство проводилось от противного, стало быть, мы и доказали следование B из посылок A®B,A.