Доказательство.

Достаточно доказать, что

\=Vik.Vj{Vi\lVj) (1.9)

\= {Vi V Y)k.{Vj V -пУ) (2)- V Vj).

[(2)- V Y)k(Vj V -пУ]) = [(2?; V У)&(-пУ V Т?})] =

Поэтому достаточно убедиться, что

h т V У)&(У V]) (Vi V 2?;-)]. (1.10)

Формула (1.10) получается из общезначимой формулы

1= [(ЛУВ)&(ВС) (ЛУС)] (1.11)

подстановками:

AVi, BY, CVj.

Следовательно, формула (1.10) общезначима. Поэтому общезначима и формула (1.9).

Теорема 1.7 доказана.

Неоднократно применяя правило получения резольвент к множеству дизъюнкт, стремятся получить пустой дизъюнкт □.

Наличие пустого дизъюнкта □ свидетельствует о получении противоречия, поскольку пустая резольвента получается из двух противоречащих друг другу дизъюнктов У и -пУ, каждый из которых логическое следствие формулы -пЛ в соответствии с правшюм

Ак.В А, В

Как следует из следующей теоремы, получение противоречия с помощью формулы ~пЛ, означает общезначимость формулы А.

Теорема 1.8 (доказательство от противного). Если Г, -А \= -L, где Г множество формул, то Т \= А-

В чем легко убедиться.

Доказательство.

Из теоремы дедукции

(Г, -пЛ 1= ±) о1= [Гк-пЛ ±).

Однако

(Г&-.Л -L) = ЫГ&с-Л) V ±) S -.(Г&-.Л) S (Г Л).

Поэтому [= (Г Л). Теорема 1.8 доказана.

Изложим по шагам

Алгоритм метода резолюций.

ТТТяг 1. Принять отрицание формулы Л, т.е. ~пЛ. Шаг 2. Привесяи формулу ~iA к конъюнктивной нормальной форме.

Шаг 3. Выписать множество ее дизъюнктов: K = {V,,V,...,Vp}.

ТТТяг 4. Выполнить анализ пар множества К по правилу: если существуют дизъюнкты T>i и Vj, один из которых (Vi) содержит литерал X, а другой (Vj) - контрарный литерал ~Х, то нужно соединить эту пару логической связкой дизъюнкции (Vi У Vj) и сформировать новый дизъюнкт - резольвенту, исключив контрарные литералы X и ~Х.

ТТТяг 5. Еош в результате соединения дизъюнктов, содержащих контрарные литералы, будет получена пустая резольвента - □, то результат достигнут (доказательство подтвердило противоречие), в противном случае включить резольвенту в множество дизъюнктов К и перейти к шагу 4.

При реализации указанного алгоритма возможны три случая:

• Среди текущего множества дизъюнктов нет резольвируемых. Это означает, что формула А не является общезначимой.

• На каком-то шаге получается пустая резольвента. Формула А общезначима.

• Процесс не останавливается, т.е. множество дизъюнкт пополняется все новыми резольвентами, среди которых нет пустых. В таком случае нельзя ничего сказать об общезначимости формулы А.

Метод резолюцдй пригоден и для доказательства того, что формула В является логическим следствием формул J-i,Тп, поскольку, как вытекает, из следствия 1.1,

jPl, ...,Тп И й о Н {Plk...&LTn В).

Для того чтобы «запустить» алгоритм метода резолюций, нужно воспользоваться тождеством

Следовательно, формула Л = ~<{Ti&i...&iTn В) общезначима, если формула ~iA = {!Fik....k.!Fnk.~~iB) является противоречием. Далее применяем описанный по шагам метод резолюций к формуле А.

Пример 1.3. Доказать, что

X, В, {СХ = -В) 1= С. (1.12)

Имеем

Л = XhBh{ChX -пВ) с, А = -nlXBiCX => -nS)fe(C)]

= XhBh{ChX = S)fe-.(-.C).

Так как

(CfeJf =-.S) = (CV-.JfV-.S), (С) = С,

-л = xBic V V -.s)fea

Следовательно,

К = {X, В, {С VXV -iS), С}. Резольвента для (-iC V -Х V -iS) и С - дизъюнкт {Х V -iB). Поэтому

К = {X, в, (-.с V V -.S), с, {Х V S)}.

Резольвента для X и V -iS) - дизъюнкт -iS, и

АГ = {Jf, S, (С V V S),С, (Jf V S), S}.

Получаем пустую резольвенту □ для дизъюнктов В и -iS. Следовательно, логическое следствие (1.12) установлено.

Пример 1.4. Доказать, что

{С&сХ = -.S) h -С?-

Имеем

Л = {С&сХ В) С,