Истинность клауз и их доказательства методом резолюций

Под высказыванием мы будем понимать грамматически правильное, однозначно понимаемое, повествовательное предложение, про которое можно сказать, что оно либо истинно, либо ложно, например:

«Киев — столица Украины»,
«Париж — столица России».

Утверждение, которое требуется доказать, в логике высказываний оформляется в виде следующего причинно-следственного отношения:
Р1, Р2, ... , Рn-1, Рn  => C                            (1.1)
где Рi — посылка (причина), С — заключение (следствие). Читается: «Если посылки Р1, Р2, ... , Рn-1, Рn  истинны, то заключение С тоже истинно» или, по-другому «Если причины Р1, Р2, ... , Рn-1, Рn  имели место, то будет иметь место и следст­вие С».
Чтобы не спутать объектное высказывание (предложение) с субъектным высказыванием, справедливость которого мы намереваемся установить, условимся предложения типа (1.1) называть клаузой (clause).

Клауза — это метапредложение, в котором использовано отношение порядка, оформленное через символ метаимпликации « => ». Как и отношение эквивалентности, отношение порядка удовлетворяет трем законам: рефлексивности:                  А => А; антисимметричности:         если , то ; транзитивности:                  если А => В и В => С, то А => С.

В отличие от эквивалентности отношение порядка предполагает выполнение закона антисимметричности, который можно записать так:
если А=>В и В=>А, то А = В.

Клауза есть именно формальная запись доказываемого предложения. Вместо букв в ней можно подставить объектные высказывания, и тогда клауза наполняется конкретным содержанием, которое уже именуется семантикой или легендой. Пример клаузы:
А->В, А => В.
Если принять, что
А = сверкнула молния, В = грянул гром, то можно составить следующую легенду:
Известно, что если сверкнула молния, то после этого грянет гром. Молния сверкнула.
Следовательно, должен и грянуть гром.

Эквивалентные формы клаузы

Над субъектом, который формулирует метапредложения, может стоять другой субъект, для которого уже предложения первого субъекта окажутся объектными. Тогда клаузу (1.1) второй субъект или метасубъект запишет для себя следующим логическим выражением:
P1,P2,…,Pn=>C
.
- (P1&P2&…&Pn)VC
Преобразовав это выражение в дизъюнкт, получим:
.
Отсюда легко находим:
.
Клауза (1.1) может быть представлена в другой эквивалентной форме:
.                                         (1.2)
В силу коммутативности конъюнкции на месте посылки Рn может оказаться любая другая, причем не одна. Например, клауза:

может быть преобразована в другую эквивалентную форму:
.                                    (1.3)
Однако клауза (1.1) по сравнению с (1.2) и другими подобными формами, типа (1.3), имеет определенные преимущества и, в частности, используется в языке логического программирования ПРОЛОГ. Ее называют хорновской. Произвольную клаузу всегда можно свести путем эквивалентных преобразований к хорновскому виду.
Если символ метаимпликации « => » клаузы (1.2) сместить в крайнее левое положение, то она превратится в тавтологию; если же его сместить в крайнее правое положение, то — в противоречие.
1 => — тавтология,
— противоречие.
Добавив в клаузу (1.1) слева 1 через «,» и сместив импликацию влево, получим смещением тавтологию.
Добавив в клаузу (1.1) справа через «;» 0 и сместив импликацию вправо, получим противоречие.

Существует пять конкретных методов доказательства справедливости логических клауз:

• аксиоматический метод,
• метод таблиц истинности,
• метод резолюций,
• метод Вонга,
• метод натурального исчисления.

Принцип резолюций

Рассмотрим еше один полуконструктивный метод доказательства истинности логических клауз, в котором используется так называемый принцип резолюций. Этот принцип играет роль аксиомы порядка и вместе с тем порождает очень эффективную конструктивную процедуру. Суть его сводится к тому, что два посылочных конъюнкта с противоположными термами всегда можно склеить в один заключительный дизъюнкт, в котором уже не будет противоположных термов:
,
где X и Y — произвольные термы или целые дизъюнкты с любым набором термов, включая ноль; А и  — произвольные термы.
Исходная клауза конструируется в форме конъюнктивного противоречия:
.

Алгоритм применения метода резолюций для доказательства клаузы

1. Преобразуем клаузу к эквивалентной форме противоречия.
2. Левую часть клаузы преобразуем к конъюнкции дизъюнкций .
3. Применяем метод резолюций к конъюнктам, имеющим форму дизъюнкции.
4. Повторяем предыдущий пункт алгоритма до тех пор пока не получим в левой части противоположные формулы в качестве конъюнктов.
5. Доказательство клаузы закончено.

Вопрос.
Докажем с помощью метода резолюций справедливость правила отделения:
 
A,A->B,-B=>0
0VA,-AVB,-BV0=>0
Здесь имеются три дизъюнкта. Склеивая их последовательно,
0VB,-BV0=>0
0V0=>0
получаем в результате ноль, который говорит о несовместимости заключения и посылок. Это как раз и свидетельствует о справедливости исходной клаузы.
Принцип резолюций целиком заменяет аксиому порядка, поскольку сама эта аксиома может быть доказана в рамках метода резолюций. Действительно,
А, В => А,     , , .
Обращаем внимание на то, что посылка В здесь вообще не используется. Это необходимо иметь в виду: необязательно использовать все посылки (их число часто бывает избыточным) — главное получить ноль.
Пусть дана клауза:
.
Доказательство ее справедливости следует начать с приведения ее в нормальную конъюнктивную форму.

Выпишем по порядку все посылки и далее начнем их склеивать согласно очередности. Справа от каждого нового дизъюнкта будем писать номера используемых дизъюнктов, получим:

Подобная стратегия поиска нуля очень непродуктивна. Если к этой же задаче подойти более творчески, то ноль обнаружится на четвертом шаге от начала поиска: