р v ~ р

и означающее "р или не р", верно всегда, независимо от смысла утверждения р.

Мы будем использовать в качестве операторов следующие символы:

~ отрицание, читается как "не"

& конъюнкцию, читается как "и"

v дизъюнкцию, читается как "или"

=> импликацию, читается как "следует"

Согласно правилам предпочтения операторов, оператор "не" связывает утверждения сильнее, чем "и", "или" и "следует".

Метод резолюции предполагает, что мы рассматриваем отрицание исходной формулы и пытаемся показать, что полученная формула противоречива. Если это действительно так, то исходная формула представляет собой тавтологию. Таким образом, основную идею можно сформулировать так: доказательство противоречивости формулы с отрицанием эквивалентно доказательству того, что исходная формула (без отрицания) есть теорема (т. е. верна всегда). Процесс, приводящий к искомому противоречию, состоит из отдельных шагов, на каждом из которых применяется резолюция.

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

(а => b) & (b => с) => (а => с)

Смысл этой формулы таков: если из а следует b и из b следует с, то из а следует с.

Прежде чем начать применять процесс резолюции ("резолюционный процесс"), необходимо представить

отрицание нашей формулы в наиболее приспособленной для этого форме. Такой формой является

конъюнктивная нормальная форма

, имеющая вид

(р1 v p2 v ...) & (q1 v q2 v ...)

& (r1 v r2 v ...) & ...

Здесь рi, qi, ri– элементарные утверждения

или их отрицания. Конъюнктивная нормальная форма есть конъюнкция членов, называемых

дизъюнктами

, например (

p1

v

p2

v ...) - это дизъюнкт.

Любую пропозициональную формулу нетрудно преобразовать в такую форму. В нашем случае это делается следующим образом. У нас есть исходная формула

(а => b) & (b => с) => (а => с)

Ее отрицание имеет вид

~ ( (а => b) & (b => с) => (а => с) )

Для преобразования этой формулы в конъюнктивную нормальную форму можно использовать следующие известные правила:

(1) х => у эквивалентно ~х v у

(2) ~(x v y) эквивалентно ~х & ~у

(3) ~(х & у) эквивалентно ~х v ~у

(4) ~( ~х) эквивалентно х

Применяя правило 1, получаем

~ ( ~ ( (a => b) & (b => с)) v (а => с) )

Далее, правила 2 и 4 дают

(а => b) & (b => с) & ~(а => с)

Трижды применив правило 1, получаем

(~ а v b) & (~b v с) & ~(~а v с)