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

Доказательство теорем сводится к доказательству того, что некоторая формула (гипотеза теоремы) является логическим следствием множества формул (допущений). То есть сама теорема может быть сформулирована следующим образом: «если истинны, то истинна и ».

Для доказательства того, что формула является логическим следствием множества формул , метод резолюций применяется следующим образом. Сначала составляется множество формул . Затем каждая из этих формул приводится к КНФ (конъюнкция дизъюнктов) и в полученных формулах зачеркиваются знаки конъюнкции. Получается множество дизъюнктов , и ищется вывод пустого дизъюнкта из . Если пустой дизъюнкт выводим из , то формула является логическим следствием формул . Если из нельзя вывести #, то не является логическим следствием формул . Такой метод доказательства теорем называется методом резолюций.
Рассмотрим пример доказательства методом резолюций. Пусть у нас есть следующие утверждения:

«Яблоко красное и ароматное.»

«Если яблоко красное, то яблоко вкусное.»

Докажем утверждение «яблоко вкусное». Введем множество формул, описывающих простые высказывания, соответствующие вышеприведенным утверждениям. Пусть

X1 — «Яблоко красное»,

X2 — «Яблоко ароматное»,

X3 — «Яблоко вкусное».

Тогда сами утверждения можно записать в виде сложных формул:

— «Яблоко красное и ароматное.»

— «Если яблоко красное, то яблоко вкусное.»

Тогда утверждение, которое надо доказать, выражается формулой X3.
Итак, докажем, что X3 является логическим следствием и . Сначала составляем множество формул с отрицанием доказываемого высказывания; получаем:

Теперь приводим все формулы к конъюнктивной нормальной форме и зачеркиваем конъюнкции. Получаем следующее множество дизъюнктов:

Далее ищем вывод пустого дизъюнкта.
Применяем к первому и третьему дизъюнктам правило резолюции:

Применяем к четвёртому и пятому дизъюнктам правило резолюции:

Таким образом пустой дизъюнкт выведен, следовательно выражение с отрицанием высказывания опровергнуто, следовательно само высказывание доказано.