![]() |
Главная -> Классическая логика 0 1 2 3 4 5 [6] 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 Доказательство. Достаточно доказать, что \=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...<n В). Для того чтобы «запустить» алгоритм метода резолюций, нужно воспользоваться тождеством Следовательно, формула Л = ~<{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 -С?- Имеем Л = {С&сХ В) С, 0 1 2 3 4 5 [6] 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 0.0118 |
|