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

Из определения вывода вытекает, что если {H1, H2, ¼, H_N}½= C, то справедливо утверждение, что (H1&H2&¼&HN)½=C, или, что ½= (H1&H2& ¼&HN)®C.

Принцип дедукции. Формула С является логическим следствием конечного множества H тогда и только тогда, когда H È {ØC} невыполнимо.

{H₁, …H_N}ú= C Û {H₁,… H_N,^ØC}ú= 0.

На основе этого утверждение строится способ доказательства, который называется доказательством "от противного" или "reDuCTio AD ABSurDuM". В этом случае в множество аксиом добавляется высказывание, равное отрицанию того, что необходимо вывести. После этого нужно доказать, что из расширенного множества аксиом выводимо противоречие.

Пример. Требуется доказать или опровергнуть вывод {`AvB, B ®C, AvD }½= CvD.

Обозначим`AvB (1), B®C (2), AvD (3). Введём ещё одно высказывание Ø(CvD)= `С&`D (4) (по правилу де Моргана). Тогда из (4)Þ`С (5), из (4)Þ`D (6), из (6) и (3) ÞA (7), из (7) и (1) ÞB (8), из (8) и (2) ÞС (9), из (8) и (9) ÞС& `С, то есть противоречие. Значит, верно, что CvD.

Доказательством "от противного" имеет смысл пользоваться, когда необходимо доказать утверждение вида дизъюнкции или следования. Первый случай, как следует из примера 2, даёт для последующего доказательства сразу два утверждения. Во втором случае из того, что Ø(B ®C) = B & `С, следует тоже два утверждения: B и `С. Используя их необходимо построить противоречие.

Задача выявления выполнимости и общезначимости формулы может оказаться довольно длительной процедурой. Заманчиво иметь более эффективный алгоритм проверки, чем последовательный просмотр всех интерпретаций.

Если формула имеет вид КНФ, то её можно рассматривать как множество дизъюнктов. Множество дизъюнктов невыполнимо тогда и только тогда, когда пустой дизъюнкт является логическим следствием из него. Невыполнимость множества S можно проверить, порождая логическое следствие до тех пор, пока не получим пустой дизъюнкт.

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

Для порождения логических следствий используется очень простая схема рассуждений. Пусть А, В, X – формулы. Предположим, что две формулы (AÚX) и (BÚØX) –истинны. Если X –истинна, то следовательно В истинна. Наоборот, если X ложна, то можно заключить, что А- истинна. В обоих случаях (AÚ В) истинна. Получается правило

{AÚX, BÚØX}ú= A Ú В,

которое можно записать в виде

{ØX vA, X vB}ú= A Ú В.

Это правило называется правилом резолюций.

Лемма. Пусть S1 и S2 –дизъюнкты нормальной формы S, l – высказывание. Если lÎS1 и ØlÎS2 , то дизъюнкт r = (S1 \ {l})îþ(S2 \ {Øl} ) является логическим следствием нормальной формы S.

Следствие. Нормальные формы S и S îþ{r} эквивалентны.

Замечание. Дизъюнкт r называется резольвентой дизъюнктов S₁ и S_2.

Алгоритм поверки на выполнимость.

2. выбираем l, S1, S2, такие что lÎS1 и ØlÎS2.

3. вычисляем резольвенту r;

4. заменяем S на S îþ{r}.

Если множество не содержит ни одной пары дизъюнктов, допускающих резольвенту, то оно выполнимо. Конечное множество S невыполнимо тогда и только тогда, когда пустой дизъюнкт может быть выведен из S с помощью резолюций.

Пример. Проверим выполнимость множества

S={P Ú q, P Ú r, Øq ÚØr, ØP}.

Дизъюнкты удобно пронумеровать:

1. P Ú q

2. P Ú r

3. Øq ÚØr

4. ØP

Вычисляем и добавляем резольвенты. В скобках указаны S₁, S₂

5. q (1,4)

6. r (2,4)

7. Øq (3,6)

8. 0 (5,7). Множество невыполнимо!