 |
Метод резолюции в исчислении высказываний
|
|
|
|
Как уже говорилось, задача проверки является ли формула исчисления высказывания теоремой требует полного перебора значений пропозициональных переменных. Таким образом, носит экспоненциальную сложность. Является NP полной. Но перебор можно существенного ограничить, оставив оценку сложности алгоритма в худшем случае прежней, но повысив среднее время. Для этого используется метод резолюций, который сводит задачу о выводимости теоремы к задаче о выполнимости КНФ. При этом вместо проверки тавтологичности формулы F используется проверка на невыполнимость формулы отр F. Если формула отр Ф не выполнима – это тавтология, есть выполнимо хотя бы на одном наборе значений, то Ф не является тавтологией, а значит и теоремой.
Теорема: F1, F2.. Fn вывод G т и тт когда выводима F1, F2.. Fn имп G. То есть когда F1, F2.. Fn имп G тожд истине
Доказательство.
Покажем правомерность правила
P имп Q, отр Q вывод отр Р
В соответствии с рассмотренной теоремой
(Р имп Кю) и отр Кю имп отр Р
| P | Q | Р имп Кю | Отр Кю | |||
Из множество формул F1, F2.. Fn выводится G т и тт, когда F1..Fn & отр G тожд равны Ложь.
В соответствии с предыд теоремой, где из F1..Fн выводится G т и тт, когда F1&Fn имп G=и
Отр (F1&Fn имп G)=л
Представим след образом
Отр(отр (F1&F2..)или G)=Л F1..Fn & отр G=Л. Чтд.
В качестве примера этой теоремы рассмотрим вывод Календа понус.
Докажем, что из P или Q, отр P выводится Q. Нужно показать, что
(P или Q) и отр P и отр Q=Л
= (P и отр Р или Q и отр P) и отр Q = Q и не Р и не Q = Л
Пусть известны цепочки химических реакций
A1 MgO+H2=Mg+H2O
A2 C+O2=CO2
A3 CO2+H2O=H2CO3
|
|
|
A4 MgO
A5 H2
A6 O2
A7 C
A8 Mg
A9 H2O
A10 CO2
A11 H2CO2
Можно ли из MgO+H2+O2+C=H2CO3
Выводится ли из А1, А2, А3, А4, А5, А6, А7 – А11. Если выводится, то
А1 и А2.. и А7 и отр А11 = Л
(А4 и А5 имп А8 и А9) и (А7 и А6 имп А10) и (А10 и А9 имп А11) и А4 и А5 и А6 и А7 и не А11
I – первая скобка и тд
А4 и А5 и (не А4 и А5) или А8и А9)=А4А5А8А9
Вносим А4А6 во вторую скобку
А6 и А7 и А10
Вносим А9А10 в третью скобку
А5А8А9А6А7А10А11и отрА11=Л
Формулу, которую проверяют на противоречие, приводят к виду КНФ. Для чего пользуются рядом эквивалентных преобразований.
А имп В=не А или В
А экв В=(АимпВ) и (ВимпА)
А и У=А
А или У=У
А и (В или С)=А и В или А и С
А или (В и С)=(А или В) и (АилиС)
Отр(А и В)=отр А или отр В
Отр (А или В)=отр А и отр В
А или (А и В)=А
А и (А или В)=А
Для проверки КНФ на противоречивость применяют алгоритм резолюций. Этот алгоритм в худшем случае будет иметь экспоненциальную сложность, однако в среднем существенно сокращает перебор по сравнению с построением таблицы истинности.
Введем ряд обозначений
Переменную или ее отрицание составим каждой элементарной дизъюнкции называют литералой. Каждую элементарную конъюнкцию называют дизъюнктом. В результате получаем что формула представленная в виде КНФ = С1 и С2 и Сн, где Си - дизъюнкты.
Каждый дизъюнкт Си = Л1 или Л2 или …Лм
Поскольку все операции известны мы можем просто считать или воспринимать КНФ как множество дизъюнктов, а каждый дизъюнкт как множество литералов. Считаем, что переменные и литералы в дизъюнктах не повторяются, так как Л или Л=Л, Л или отр Л=И. точно также считаем, что не повторяются дизъюнкты. С и С=С
Пусть дано два дизъюнкта
С1=Л или Л2,1или Л3,1.. или Лн1,1
С2 = отр Л или или Л2,2 или Л3,2 или Лн2,2
Переменная и ее отрицание, входящие в разные дизъюнкты называется контроальной парой. Тогда резольвентой дизъюнктов С1 и С2 будет дизъюнкт, составленный из всех их литералов, кроме контральной пары.
R(C1,C2)=Л2,1 или Л3,1 или Лн1,1 или Л2,2 или Л3,2 или Лн2,2
|
|
|
При этом не рассматриваются дизъюнкты, в которой более одной контральной пары, так как цель нахождения резольвенты – это получить опровержение формулы.
Резольвента является следствием своих дизъюнктов
С1 и С2 имп R(C1,C2)=И
С1 и С2=Л, тогда формула И
С1 и С2=И
С1 = Л или Л2,1 или Лн1,1
С2 = Л или Л2,2 или Лн2,1
Если С1=И, за счет какого-то из литералов, начиная со второго, то этот литерал войдет в резольвенту, а значит резольвента тоже будет И. Если С1 истинно за счет литерала Л, то литерал отрицания Л в С2 ложь, а значит С2 истинно за счет какого-то другого литерала, а он войдет в резольвенту и резольвента будет истинна. Формула истинна
Следствие: дано С1 и С2.. Сн и R(Ci, Cj), тогда С1 и С2..Сн экв
С1 и 2 и.. Сн и R(Ci,Cj), то есть резольвенту можно добавлять в список дизъюнктов.
Доказательство:
Если левая часть ложь, правая часть ложь. Если левая часть истина, то по только что доказанной теореме будет истинна и резольвента, а значит и правая часть.
Пусть дано множество дизъюнктов. Тогда резолютативным выводом дизъюнкта D будет цепочка дизъюнктов А1, А2..Ак (D), где каждый дизъюнкт или является исходным или является резольвентой каких-либо двух предыдущих дизъюнктов.
Теорема о полноте метода резолюций. КНФ противоречива т и тт, когда из множества его дизъюнктов результативно выводится пустой дизъюнкт.
Доказательство:
Если выводится пустой дизъюнкт, то в КНФ присутствуют дизъюнкты С1=Л, С2=отр Л. С1 и С2 и..Сн=Ложь
Следует помнить, что каждый раз получая резольвенту в соответствии с ранее доказанными утверждениями, мы добавляем ее в число дизъюнктов.
Покажем, что из резольвенты выводится пустой дизъюнкт. Доказательство будем вести по индукции. Будем использовать специальный параметр K(S)=сумм кол-во вхождение литералов – кол-во дизъюнктов
Докажем справедливость при К(S)=0. тогда в каждом дизъюнкте только один литерал и формула имеет вид Л1 и Л2.. и Лн. Эта формула может быть противоречива т и тт, когда в ней встречается пара литералов Л и отр Л, а значит в данной КНФ пустой дизъюнкт выводится.
Пусть k<=m, докажем для формулы, где k=m+1>0. Если к>0, то хотя бы один дизъюнкт содержит более одного литерала, пусть будет С1.
Тогда С1=Л или С’, где С’остальная часть.
S=С1..и Сн=С1 и S’=(Л или С’) и S’=Л и S’(1) или C’и S’(2)
|
|
|
Так как исходные значения противоречивы КНФ 1 и 2. По предположению индукции в каждой из них выводим пустой дизъюнкт. Берем вывод пустого дизъюнкта из формулы 2 и применяем его к исходной КНФ. Она отличается от формулы 2 только наличием литерала Л в С1. Значит по результатам вывода получится либо пустой дизъюнкт, либо Л. Чтд.
Запишем алгоритм метода резолюций для логики высказываний. Предполагается, что уже построена формула, которую нужно проверить на противоречие и она в виде КНФ.
1. находим всевозможные резольвенты для дизъюнктов КНФ. При этом, есть среди резольвент встретился пустой дизъюнкт, завершаем работу с успехом. Формула противоречие.
2. Если множество резольвент пустое, то останавливаем алгоритм с неудачей. Формула выполнима.
3. добавляем полученные резольвенты к числу дизъюнктов, переходим к 1
|
|
|
