3.2.2 Схемы исчисления высказываний

Введение допущения

Д ля доказательства А В допускаем, что А. Тогда докажем, что из А следует В (т.е. А В является тавтологией).

Резолюция – это тавтология вида:

[ ( X   A)  ( Y  A) ]  X  Y =  [ ( X   A)  ( Y  A) ]  X  Y =

= [ ( X  A)  (  Y   A) ]  X  Y = [ ( X  X)  ( A  X) ]  [ ( Y  Y) 

 (  A  Y) ] = A  X   A  Y = «истина»  X  Y = «истина».

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

Вместо логического вывода истинности А  В доказывают, что ложно  (А  В), т.е. ложно:  (А  В) =  ( А  В) = А   В.

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

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

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

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

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

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

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

А  В = (А  В)  (В  А); А  В =  А  В;

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

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

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

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

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

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

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

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

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

А, В  С |– А  В , С .

А  ( В  С )   (А  В )   С = (А  )  ( В  С )  ( А   В )  ( С  ) =

А    В  

В  С    = 

 А   В В  

 С  

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