1.9.2. Доказательство введением допущения

Для доказательства истинности импликации ABдопускают истинностьAи доказывают истинностьB. ЕслиBдоказано, то импликация истинна. Этот метод базируется на двух теоремах.

Теорема1.ABтогда и только тогда, когдаAB

Т.е. доказуемость заключения Bиз допущенияAэквивалентна доказуемости следованияBизAбез дополнительных допущений. Истинность этой теоремы проверяется по таблице истинности.

Теорема 2. A₁, A₂, ... A_nBтогда и только тогда, когда(A₁^A₂^...^A_n)B.

Эта теорема есть расширенная формулировка первой.

1.9.3. Приведение к противоречию

Доказательство введением допущения в приведенной выше формулировке называется методом прямой волныи имеет определенный недостаток: сложно запрограммировать его для ЭВМ так, чтобы вывод всегда шел по оптимальному пути. Если не ограничить глубину вывода, он может привести к массе ненужных результатов, не достигнув искомого.

В ряде случаев полезнее метод поиска от цели, основанный на равнозначности (BC)(~C~B). Т.е., допустив ~C, доказывают ~B. Если ~Bудается доказать, то доказанным считаетсяBC.

Комбинацией этих методов является метод приведения к противоречию. Здесь допускают, что ~(BC). Получив противоречие, делают вывод, что исходное предположение не верно, а верна его инверсия, т.е.BC.

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

Метод резолюций основан на правиле, называемом принципом резолюций. Принцип резолюций включает в себя принцип отыскания частных случаев (правило подстановки) и принцип силлогизма, который формулируется следующим образом (см. теоремы из п. 1.9.2):

(XA)(Y~A)(XY)

(XA),(Y~A) (XY)

Суть метода доказательства, основанного на принципе резолюций в следующем.

Исходные данные: множество посылок H= {H₁,H₂, ...H_n}, заключение С.

Необходимо доказать: (HC)(H₁,H₂, ...H_nC).

Для этого произведем следующие преобразования последней формулы:

H₁, H₂, ... H_nC = ~(H₁H₂...H_n)C = ~((H₁H₂...H_n)~C)

и применим метод приведения к противоречию, т.е. попытаемся доказать ложность этой импликации, иными словами, попытаемся доказать, что

H₁H₂...H_n~C = T

Основные этапы метода резолюций:

1. Составляется формула из всех посылок H_iи отрицания заключения ~C. Она приводится к КНФ.

2. Каждый дизъюнкт КНФ выписывается с новой строки.

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

4. Если в результате остаются дизъюнкты типа Pи ~P, очевидно, что их конъюнкция равнаF, или можно сказать, что результатом их конъюнкции будет пустой дизъюнкт. Значит, наше предположение не верно, а верна доказываемая импликация.

Алгоритм получения резольвенты (этап 3) для ИП выглядит следующим образом:

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

2. Находится минимальная подстановка констант вместо переменных, которая делает литеры идентичными, но с противоположными знаками.

3. Подстановка выполняется в обоих выбранных предложениях.

4. Если в предложении (дизъюнкте) имеются одинаковые литеры, они вычеркиваются, кроме одной (согласно правилу идемпотентности).

5. В двух выбранных предложениях вычеркиваются взаимоинверсные литеры и производится образование нового дизъюнкта согласно принципу резолюций.

С использованием принципа резолюций можно разработать программу, которая за конечное число шагов найдет резольвенты двух предложений. Принцип резолюций является достаточным как для нахождения доказательства, так и для отыскания следствий. Цель процедуры нахождения доказательства состоит в том, чтобы показать невыполнимость отрицания подлежащей доказательству теоремы, т.е. это отрицание должно приводить к противоречию. Робинсон доказал, что если конечное множеств предложений несовместимо, то противоречие может быть обнаружено за конечное число применений принципа резолюций.

Пример для ИВ.Доказать (PQ),(PS),(ST),(TR)(QR)

1. (PQ)(PS)(ST)(TR)~(QR) = (~PQ)(PS)(~ST)(~TR)~Q~R

2. Запишем дизъюнкты: 1) ~PQ 2) PS 3) ~ST 4) ~TR 5) ~Q 6) ~R

3. Производим слияние дизъюнктов: 7) Из (1) и (2): QS8) Из (3) и (4): ~SR9) Из (7) и (8):QR10) Из (5) и (9):R11) Из (6) и (10): # =F

4. Делаем вывод об истинности импликации.