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

Доказательство от противного

Вместо логического вывода истинности А É В доказывают, что ложноù(А É В), т.е. ложно: ù(А É В) = ù(ù А Ú В) = А Ù ù В.

Нужно доказать ложность конъюнкции, состоящей из исходных посылок и отрицания заключения: А₁, А₂,…, А_n |– В Þ А₁ Ù А₂ Ù…Ù А_n Ùù В.

Основан на схеме доказательства от противного.

Алгоритм следующий:

1. Строится конъюнкция, состоящая из исходных посылок и отрицания заключения.

2. Она приводится к КНФ. Для чего :

· устраняются ипмпликация и эквиваленция по следующим соотношениям:

А ~ В = (А É В) Ù (В É А); А É В = ù А Ú В;

· по закону де Моргана опускаются все отрицания до переменных;

· используя ассоциативный, коммутативный, дистрибутивный законы, раскрываются скобки;

3. Выписываются дизъюнкты полученной КНФ каждый в отдельную строку.

Примечание: если дизъюнкт состоит из одной буквы, то дополняют его пустым дизъюнктом ÿ, который соответствует ложному высказыванию.

4. Выбирают из данных дизъюнктов пару так, чтобы она образовывала исходные посылки метода резолюции, т.е., чтобы в выбранной паре посылка присутствовала с отрицанием и без отрицания: Х Ú А, Y Ú ù А.

5. К выбранной паре применяется метод резолюции. Получают новый дизъюнкт, который далее рассматривается наравне с оставшимися дизъюнктами.

6. Повторяют пункты 4 и 5 до тех пор, пока не получат пустой дизъюнкт.

7. Если в результате выполнения пунктов 4 – 6 выводят пусто дизъюнкт, т.е. ложь, то исходный логический вывод считается доказанным, т.к. предполагалось отрицание исходной посылки. Доказательство лжи от противного равносильно доказательству истины посылки. В противном случае вывод отвергается.

Пример: Доказать методом резолюции истинность высказывания:

А, В Ú С |– А Ù В , С .

А Ù ( В Ú С ) Ù ù (А Ù В ) Ù ù С = (А Ú ÿ) Ù ( В Ú С ) Ù (ù А Ú ù В ) Ù (ù С Ú ÿ) =

А Ú ÿ ù В Ú ÿ

В Ú С ÿ Ú ÿ = ÿ

ù А Ú ù В В Ú ÿ

ù С Ú ÿ

Доказана ложь, значит исходное положение – истина.