3.09 Использование правила резолюции. для логического вывода

Пусть у нас есть набор высказываний, как атомарных, так и сложных. На основе этих высказываний делается некоторый вывод или заключение. Нам необходимо выяснить истинность или ложность этого заключения.

Применение для этих целей метода резолюции имеет следующий алгоритм:

Будем использовать доказательство от противного, т. е. счита­ем, что заключение ложно.

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

А) устраняем символы ® и «, если они присутствуют в исходных высказываниях:

А ® В = B; A « B = (A ® В)(B ® A) = ( B)(A);

Б) устраняем цепочки АBC, если они есть, используя дистрибутивный закон:

АBC = А(BC) = (АB)(AC);

В) устраняем отрицания высказываний, если они есть, по правилу де Моргана:

() = ; () = ;

3. Теперь каждое высказывание превратилось в конъюнкцию дизъюнктов.

Выписываем каждый дизъюнкт с новой строки. Все они истин­ны, так как конъюнкция истинна по предположению.

4. Каждый дизъюнкт – это дизъюнкция, состоящая из исходного высказывания и его отрицания. Именно к ним применим метод резолюций. Берем любые два дизъюнкта, содержащие один и тот же атом, но с противоположными знаками. Применяя метод резолюций, удаляем его из двух данных дизъюнктов:

ХYZP и XW Þ XYZW;

А и Y Þ Y.

5. Продолжаем этот процесс, пока у нас не останется выска­зывания Р и для одного единственного атома Р. Применяя резо­люцию к ним, получим пустой дизъюнкт, выражающий противоречие. Это завершает доказательство от противного. Из Р и выводим ложь.

Пример.

У нас есть набор высказываний:

Р Q; Р ® R; Q ® S. Надо сделать вывод об истинности высказывания R S.

1. Будем считать, что R S ложно, т. е. = Т.

2. Приводим посылки и отрицание заключения к нормальной форме:

Р ® R = R;
Q ® S = S;
= .

3. Выписываем дизъюнкты на отдельные строки и нумеруем их:

P Q (1)
R (2)
S (3)

И два одночленных дизъюнкта

(4)
(5)

Все пять дизъюнктов имеют значение Т.

4. Группируем дизъюнкты, содержащие некоторый атом с противоположными знаками, и применяем правило резолюции:

- (2) + (4) R и Þ (6)
- (1) + (6) P Q и Þ Q (7)
- (3) + (5) S и Þ (8)

И, наконец, из (7) и (8) получаем пустой дизъюнкт:

Q и Þ ð. Это свидетельствует о ложности нашей посылки = Т. Следовательно, вывод R S является истинным.

ð – Пустой дизъюнкт.

< Предыдущая		Следующая >