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

1930 г. Эрбран. Метод доказательства теорем в ФС первого порядка.

Идея: чтобы получить некоторое заключение C, исходя из гипотез H1, H2,…Hn, т.е. доказать теорему T:

H1 H2 Hn C, достаточно доказать противоречивость формулы:

H1 H2 Hn C,

в которой отрицание заключения добавлено к исходным гипотезам. Это может оказаться проще прямого вывода.

Соображения тривиальны: доказательство выполнимости множества G H ( G H) – это опровержение его невыполнимости, т.е. невыполнимости ( G H), что эквивалентно G H.

Установление невыполнимости множества предложений осуществляется посредством принципа резолюций – специальной процедуры логического вывода новых предложений из множества исходных.

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

Алгоритм вывода по методу резолюций

Правила вывода ИП и метод резолюций

Пример. Доказать истинность заключения A; В; (С A B)

С.

1)A - посылка;

2)B - посылка;

3)C A B = ( C A B) - посылка;

4)( C) = C - отрицание заключения;

5)множество дизъюнктов: K={A; B; ( C A B); C};

6)A ( C A B)=( С B) - резольвента из 1) и 3);

7)K1={A; B; ( C A B); C; ( С B)};

8)B ( С B)= C - резольвента из 2) и 6);

9)K2={A; B; ( C A B); C; ( С B); C };

10)С C = - пустая резольвента из 4) и 7).

Пример. Работа автоматического устройства, имеющего три клапана А, В и С, удовлетворяет следующим условиям: если не срабатывают клапаны А или В или оба вместе, то срабатывает клапан С; если срабатывают клапаны А или В или оба вместе, то не срабатывает клапан С. Следовательно, если срабатывает клапан С, то не срабатывает клапан В.

Доказать истинность заключения: ((¬А ¬В ¬А В) С), ((А В А В) С)

(С ¬В)