Принцип резолюции для логики высказываний

Легко проверяется, что формула

[(А В)&(B C)] (A C) (1)

общезначима, т. е. является теоремой ИВ.

Лемма. Пусть в КНФ K(X ₁, X ₂ ,…,X_n) входят дизъюнкты D ₁ и D ₂ ,причем D ₁ представим в виде D ₁ ^' X_i, а D ₂ – в виде D ₂ ^' X_i. Тогда логическим следствием входящих в КНФ утверждений (дизъюнктов) является дизъюнкт D ₁ ^' D ₂ ^'.

Действительно, дизъюнкт D ₂ ^' X_i эквивалентен формуле X_i D ₂^'. В формулу (1) вместо A подставим D ₁ ^', вместо В - X_i и вместо С - D ₂ ^'. Получаем следующую теорему ИВ:

[(D ₁ ^' X_i)&(X_i D ₂ ^')] (D ₁ ' D ₂ ^').

Так как утверждения D ₁ ^' X_i и X_i D₂ ^' входят в состав КНФ в качестве логического следствия образующих КНФ K(X₁, X₂,…,X_n) дизъюнктов, получаем D₁^' D₂^'. Лемма доказана.

Формула D ₁^' D ₂^' называется резольвентой формул D₁= D₁^' X_i и D₂= D₂^' X_{i .} Резольвента D₁' D ₂^' - логическое следствие дизъюнктов D ₁ и D ₂.

Резольвентой однолитерных дизъюнктов X и X является противоречивая формула (пустой дизъюнкт) ÿ.

Идея принципа резолюции заключается в проверке, выводим ли из дизъюнктов, составляющих КНФ K (X ₁, X ₂,…, X_n,), пустой дизъюнкт. Вывод конструируется последовательным построением резольвент. Выводимость из КНФ пустого дизъюнкта означает ее противоречивость.

Пример 3. Задана КНФ K (P,Q) = (Р Q) & ( Р Q) & (Р Q) & ( Р Q). Требуется доказать ее противоречивость,

В состав рассматриваемой КНФ входят четыре дизъюнкта:

1) Р Q;

2) Р Q;

3) Р Q;

4) Р Q.

Строим следующие резольвенты (для каждой записываемой резольвенты в скобках указываются номера исходных для нее дизъюнктов):

5) Q (1,2);

6) Q (3,4);

7) ÿ (5,6).

Из составляющих КНФ K (P,Q) дизъюнктов в качестве логического следствия выведенпустой дизъюнкт. Это означает противоречивость данной КНФ.

В дизъюнктах D ₁^' X_i и D ₂^' X_i вхождения переменой X_i именуются контрарными. Так, в дизъюнктах 1) и 2), 3) и 4) контрарны вхождения буквы P;в дизъюнктах 5) и 6) контрарны вхождения буквы Q. Пустой дизъюнкт есть резолюция контрарных литер.

Пример 4. Известно следующее: прямая L ₁либо параллельна прямой L ₂, либо совпадает с ней; параллельные прямые не имеют общих точек; прямые L ₁ и L ₂ имеют общую точку. Методом резолюции требуется доказать, что прямые L ₁ и L ₂ совпадают.

Исходные предположения на языке ИВ записываются следующим образом:

1) A B;

2) A C;

3) C.

Требуется доказать справедливость утверждения B. Утверждение B является логическим следствием предположений 1),2),3) тогда и только тогда, когда формула

(A B)&(A C)& C & B

невыполнима.

Так как формула A C эквивалентна A C, нам требуется показать противоречивость следующей совокупности дизъюнктов:

1') A B;

2') A C;

3') C;

4') B.

Конструируем резольвенты:

5') A (1', 4');

6') C (5', 2');

7') ÿ (3', 6').

Итак, прямые L ₁ и L ₂ действительно совпадают.

Пример 5. Если футбольная команда A выигрывает, то город А ' торжествует; если команда В выигрывает, то торжествует город B '. Выигрывает либо команда A, либо команда В. Однако, если команда A выигрывает, то город В ' не торжествует; если выигрывает команда В, то город А ' не торжествует. Требуется доказать, что город А ' торжествует тогда и только тогда, когда не торжествует город В '.

Запишем посылки и заключения на языке ИВ:

1) A А';

2) В В';

3) A B;

4) A В';

5) В А';

6) (А' В')&( В' А').

Отметим, что

[(А' В')&( В' А')]= (А '& В ') ( В' А')=

(А ' В ')& ( А' В').

Таким образом, требуется доказать противоречивость следующей совокупности дизъюнктов:

1) A А'; 2) В В'; 3) A B; 4) A В';

5) В А'; 6) А' В'; 7) В' А'.

Конструируем резольвенты:

8) А' В (1,3);

9) В А' (2,6);

10) А' (8,9);

11) A А' (3,5);

12) A А' (4,7);

13) А ' (11,12);

14) ÿ (10,13).

Решение закончено.

Теорема о полноте принципа резолюций. Если конечная совокупность дизъюнктов противоречива, то данный факт можно доказать, основываясь на принципе резолюции, т. е. путем последовательного конструирования резольвент, вплоть до получения пустого дизъюнкта.

Верхняя оценка временной вычислительной сложности, основанная на принципе резолюции алгоритма проверки противоречивости КНФ, экспоненциальна, что связано с NР— полнотой рассматриваемой проблемы.

При реализации данного алгоритма осуществляется поиск вывода пустого дизъюнкта. Некоторые направления поиска могут оказаться тупиковыми, полученные при этом результаты в найденном выводе пустого дизъюнкта не используются.

Так возникает вопрос о построении стратегий поиска, обеспечивающих в случае противоречивости рассматриваемой совокупности утверждений достаточно быстрый вывод пустого дизъюнкта (по оценке "в среднем").

Дата добавления: 2015-06-27