Лекции В.А. Захарова (1157993), страница 14
Текст из файла (страница 14)
. . , DN } — система дизъюнктов.Резолютивным выводом из системы дизъюнктов S называетсяконечная последовательность дизъюнктов0D10 , D20 , . . . , Di0 , Di+1, . . . , Dn0 ,в которой для любого i, 1 ≤ i ≤ n, выполняется одно из трехусловий:1. либо Di0 — вариант некоторого дизъюнкта из S;2. либо Di0 — резольвента дизъюнктов Dj0 и Dk0 , где j, k < i;3. либо Di0 — склейка дизъюнкта Dj0 , где j < i.Дизъюнкты D10 , D20 , . . .
, Dn0 считаются резолютивновыводимыми из системы S.РЕЗОЛЮТИВНЫЙ ВЫВОДПример резолютивного вывода.S = {D1 , D2 , D3 }D1 = P(x, f (y )) ∨ R(y ),D2 = ¬R(y ),D3 = ¬P(f (x), z) ∨ ¬P(y , y ).Резолютивный вывод из S1.2.3.4.5.6.D10D20D30D40D50D60= P(x1 , f (y1 )) ∨ R(y1 ), вариант дизъюнкта D1= ¬R(y2 ), вариант дизъюнкта D2= P(x3 , f (y3 )), резольвента дизъюнктов D10 , D20= ¬P(f (x4 ), z4 ) ∨ ¬P(y4 , y4 ), вариант дизъюнкта D3= ¬P(f (x5 ), f (x5 )), склейка D40= , резольвента дизъюнктов D30 и D50Здесь — пустой дизъюнкт , тождественная ложь.РЕЗОЛЮТИВНЫЙ ВЫВОДПример резолютивного вывода.А почему пустой дизъюнкт — это тождественная ложь?А потому, что каждый дизънкт D = L1 ∨ · · · ∨ Ln равносиленутверждению L1 ∨ · · · ∨ Ln ∨ false.Поэтому резольвентой дизъюнктов D1 = L ∨ false иD2 = ¬L ∨ false будет дизъюнкт D0 = false.Этот дизъюнкт не содержит ни одной литеры, и поэтомуназывается пустым дизънктом .РЕЗОЛЮТИВНЫЙ ВЫВОДОбратите внимание на то, что я постоянно переименовываюпеременные так, чтобы каждый дизъюнкт резолютивноговывода содержал свою индивидуальную систему переменных!Резолютивный вывод из S1.2.3.4.5.6.D10D20D30D40D50D60= P(x1 , f (y1 )) ∨ R(y1 )= ¬R(y2 )= P(x3 , f (y3 ))= ¬P(f (x4 ), z4 ) ∨ ¬P(y4 , y4 )= ¬P(f (x5 ), f (x5 ))=Зачем это нужно?РЕЗОЛЮТИВНЫЙ ВЫВОДВсе дело в том, что все переменные дизъюнктов связаныкванторами ∀, и поэтому их имена можно достаточнопроизвольно изменять, полностью сохраняя смысл формул.Однако, случайное совпадение имен переменных (коллизия)может привести к тому, что резольвенту дизъюнктов построитьне удастся.Пусть S = {D1 = P(x), D2 = ¬P(f (x))}.1.
D10 = P(x)2. D20 =¬P(f (x))3. НОУ P(x), P(f (x)) = ∅,1. D100 = P(x1 )2. D200 = ¬P(f (x2 ))и поэтому D10 , D20не имеют резольвенты.резольвента D100 , D200 .3. D300 = Итак, наш девиз:НОВЫЙ ДИЗЪЮНКТ — НОВЫЕ ПЕРЕМЕННЫЕ.РЕЗОЛЮТИВНЫЙ ВЫВОДРезолютивный вывод называется успешным (или, по другому,резолютивным опровержением ), если этот вывод оканчиваетсяпустым дизъюнктом .В чем же состоит успех такого резолютивного вывода и чтопри этом опровергнуто?Успешный вывод — это свидетельство того, что системадизъюнктов S противоречива и опровергнуто предположениео ее выполнимости!Но это придется обосновать.КОРРЕКТНОСТЬ РЕЗОЛЮТИВНОГОВЫВОДАТеорема корректности резолютивного выводаЕсли из системы дизъюнктов S резолютивно выводим пустойдизъюнкт , то S — противоречивая система дизъюнктов.Доказательство теоремыПустой дизъюнкт тождественно ложен, т.е.
не имеет моделей.Покажем, что каждый дизъюнкт, резолютивно выводимый изS, является логическим следствием S. ТогдаS |= ,и это означает, что S также не имеет моделей, т.е. являетсяпротиворечивой системой.Остается доказать две леммы.КОРРЕКТНОСТЬ РЕЗОЛЮТИВНОГОВЫВОДАЛемма 1.Если D0 — резольвента дизъюнктов D1 и D2 , то D1 , D2 |= D0Доказательство леммы 1.D1 = D10 ∨L1 , D2 = D20 ∨¬L2 , θ ∈ НОУ(L1 , L2 ), D0 = (D10 ∨D20 )θТаким образом, L1 θ = L2 θ = L0 .Поэтому мы получаем следующие соотношенияD1 , D2 |= D1 θ,D1 , D2 |= D10 θ ∨ L1 θ,D1 , D2 |= D10 θ ∨ L0 ,D1 , D2 |= D10 θ ∨ D20 θ ∨ L0 ,D1 , D2 |= D2 θD1 , D2 |= D20 θ ∨ ¬L2 θD1 , D2 |= D20 θ ∨ ¬L0D1 , D2 |= D10 θ ∨ D20 θ ∨ ¬L0D1 , D2 |= D10 θ ∨ D20 θD1 , D2 |= D0Вот и все.
КОРРЕКТНОСТЬ РЕЗОЛЮТИВНОГОВЫВОДАЛемма 2.Если D0 — склейка дизъюнкта D, то D |= D0 .Доказательство леммы 2.Самостоятельно.ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙПример.Рассмотрим формулу ϕ∀x∀y ∃v ∀u(A(u, v ) → B(y , u))&(¬∃wA(w , u) → ∀zA(z, v ))→ ∃yB(x, y )ЗадачаПроверить, верно ли, что |= ϕ.РешениеМетодом резолюций.ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешениеЭтап 1. Покажем, что формула ϕ1 = ¬ϕ противоречивая.ϕ1 = ¬∀x∀y ∃v ∀u(A(u, v ) → B(y , u)) &(¬∃wA(w , u) → ∀zA(z, v ))→ ∃yB(x, y )ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешениеЭтап 2.
Приведем ϕ1 к ПНФ ϕ2 .Исходная формула¬∀x∀y ∃v ∀u(A(u, v ) → B(y , u)) &(¬∃wA(w , u) → ∀zA(z, v ))→ ∃yB(x, y )ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешениеЭтап 2. Приведем ϕ1 к ПНФ ϕ2 .Переименование переменных¬∀x∀y 0 ∃v ∀u(A(u, v ) → B(y 0 , u)) &(¬∃wA(w , u) → ∀zA(z, v ))→ ∃y 00 B(x, y 00 )ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешениеЭтап 2.
Приведем ϕ1 к ПНФ ϕ2 .Удаление импликаций¬∀x¬∀y 0 ∃v ∀u(¬A(u, v ) ∨ B(y 0 , u)) &(¬¬∃wA(w , u) ∨ ∀zA(z, v ))∨ ∃y 00 B(x, y 00 )ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешениеЭтап 2. Приведем ϕ1 к ПНФ ϕ2 .Продвижение отрицаний∃x∀y 0 ∃v ∀u(¬A(u, v ) ∨ B(y 0 , u)) &(∃wA(w , u) ∨ ∀zA(z, v ))& ∀y 00 ¬B(x, y 00 )ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешениеЭтап 2. Приведем ϕ1 к ПНФ ϕ2 .Вынесение кванторовϕ2 =∃x∀y 0 ∃v ∀u∃w ∀z∀y 00(¬A(u, v ) ∨ B(y 0 , u)) &(A(w , u) ∨ A(z, v )) &¬B(x, y 00 )ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешениеЭтап 3. Приведем ϕ2 к ССФ ϕ3 .ϕ3 =∀y 0∀u∀z∀y 00(¬A(u, f (y 0 )) ∨ B(y 0 , u)) &(A(g (y 0 , u), u) ∨ A(z, f (y 0 ))) & ¬B(c, y 00 )ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешениеЭтап 4. Формирование системы дизъюнктов Sϕ .Sϕ =nD1 = ¬A(u, f (y 0 )) ∨ B(y 0 , u),D2 = A(g (y 0 , u), u) ∨ A(z, f (y 0 )), oD3 = ¬B(c, y 00 )ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешениеЭтап 5. Резолютивный вывод из Sϕ .Sϕ =nD1 = ¬A(u, f (y 0 )) ∨ B(y 0 , u),D2 = A(g (y 0 , u), u) ∨ A(z, f (y 0 )), oD3 = ¬B(c, y 00 )1.
D10 = ¬A(u1 , f (y10 )) ∨ B(y10 , u1 ),2. D20 = A(g (y20 , u2 ), u2 ) ∨ A(z2 , f (y20 )),3. D30 = A(g (y30 , f (y30 )), f (y30 )),4. D40 = B(y40 , g (y40 , f (y40 ))),5. D50 = ¬B(c, y500 ),6. D60 = .ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешениеЭтап 5. Резолютивный вывод из Sϕ .Sϕ =nD1 = ¬A(u, f (y 0 )) ∨ B(y 0 , u),D2 = A(g (y 0 , u), u) ∨ A(z, f (y 0 )), oD3 = ¬B(c, y 00 )1. D10 = ¬A(u1 , f (y10 )) ∨ B(y10 , u1 ), (вариант D1 )2.
D20 = A(g (y20 , u2 ), u2 ) ∨ A(z2 , f (y20 )),3. D30 = A(g (y30 , f (y30 )), f (y30 )),4. D40 = B(y40 , g (y40 , f (y40 ))),5. D50 = ¬B(c, y500 ),6. D60 = .ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешениеЭтап 5. Резолютивный вывод из Sϕ .Sϕ =nD1 = ¬A(u, f (y 0 )) ∨ B(y 0 , u),D2 = A(g (y 0 , u), u) ∨ A(z, f (y 0 )), oD3 = ¬B(c, y 00 )1. D10 = ¬A(u1 , f (y10 )) ∨ B(y10 , u1 ),2. D20 = A(g (y20 , u2 ), u2 ) ∨ A(z2 , f (y20 )), (вариант D2 )3. D30 = A(g (y30 , f (y30 )), f (y30 )),4.
D40 = B(y40 , g (y40 , f (y40 ))),5. D50 = ¬B(c, y500 ),6. D60 = .ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешениеЭтап 5. Резолютивный вывод из Sϕ .Sϕ =nD1 = ¬A(u, f (y 0 )) ∨ B(y 0 , u),D2 = A(g (y 0 , u), u) ∨ A(z, f (y 0 )), oD3 = ¬B(c, y 00 )1. D10 = ¬A(u1 , f (y10 )) ∨ B(y10 , u1 ),2. D20 = A(g (y20 , u2 ), u2 ) ∨ A(z2 , f (y20 )),3. D30 = A(g (y30 , f (y30 )), f (y30 )), (склейка D20 )4.
D40 = B(y40 , g (y40 , f (y40 ))),5. D50 = ¬B(c, y500 ),6. D60 = .ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешениеЭтап 5. Резолютивный вывод из Sϕ .Sϕ =nD1 = ¬A(u, f (y 0 )) ∨ B(y 0 , u),D2 = A(g (y 0 , u), u) ∨ A(z, f (y 0 )), oD3 = ¬B(c, y 00 )1. D10 = ¬A(u1 , f (y10 )) ∨ B(y10 , u1 ),2.
D20 = A(g (y20 , u2 ), u2 ) ∨ A(z2 , f (y20 )),3. D30 = A(g (y30 , f (y30 )), f (y30 )),4. D40 = B(y40 , g (y40 , f (y40 ))), (резольвента D10 и D30 )5. D50 = ¬B(c, y500 ),6. D60 = .ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешениеЭтап 5. Резолютивный вывод из Sϕ .Sϕ =nD1 = ¬A(u, f (y 0 )) ∨ B(y 0 , u),D2 = A(g (y 0 , u), u) ∨ A(z, f (y 0 )), oD3 = ¬B(c, y 00 )1. D10 = ¬A(u1 , f (y10 )) ∨ B(y10 , u1 ),2. D20 = A(g (y20 , u2 ), u2 ) ∨ A(z2 , f (y20 )),3. D30 = A(g (y30 , f (y30 )), f (y30 )),4. D40 = B(y40 , g (y40 , f (y40 ))),5.
D50 = ¬B(c, y500 ), (вариант D3 )6. D60 = .ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешениеЭтап 5. Резолютивный вывод из Sϕ .Sϕ =nD1 = ¬A(u, f (y 0 )) ∨ B(y 0 , u),D2 = A(g (y 0 , u), u) ∨ A(z, f (y 0 )), oD3 = ¬B(c, y 00 )1. D10 = ¬A(u1 , f (y10 )) ∨ B(y10 , u1 ),2. D20 = A(g (y20 , u2 ), u2 ) ∨ A(z2 , f (y20 )),3. D30 = A(g (y30 , f (y30 )), f (y30 )),4. D40 = B(y40 , g (y40 , f (y40 ))),5. D50 = ¬B(c, y500 ),6. D60 = . (резольвента D40 и D50 )ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешениеЗаключение. Успешный резолютивный вывод из Sϕ означает,что Sϕ — противоречивая система дизъюнктов.Значит, ϕ1 = ¬ϕ — невыполнимая формула.Значит, ϕ — общезначимая формула,|= ϕ.ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙВопрос полнотыА можно ли таким способом проверять общезначимость любыхформул?Этот вопрос может быть уточнен так:1.
Верно ли, что для любой общезначимой формулы ϕможно построить успешный резолютивный вывод изсоответствующей системы дизъюнктов Sϕ ?2. Верно ли, что в том случае, когда формулы ϕнеобщезначима (система дизъюнктов Sϕ выполнима), мысможем каким-то образом обнаружить невозможностьпостроения успешного резолютивного вывода?КОНЕЦ ЛЕКЦИИ 9.Îñíîâûìàòåìàòè÷åñêîéëîãèêèèëîãè÷åñêîãîïðîãðàììèðîâàíèÿËÅÊÒÎÐ: Â.À. ÇàõàðîâËåêöèÿ 10.Ïîëíîòà ðåçîëþòèâíîãî âûâîäà.Ïðèìåíåíèå ìåòîäà ðåçîëþöèé.ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀÒåîðåìà î ïîëíîòå ðåçîëþòèâíîãî âûâîäàÅñëè S ïðîòèâîðå÷èâàÿ ñèñòåìà äèçúþíêòîâ, òî èç Sðåçîëþòèâíî âûâîäèì ïóñòîé äèçúþíêò .Äîêàçàòåëüñòâî.Åñëè S ïðîòèâîðå÷èâàÿ ñèñòåìà äèçúþíêòîâ, òî ñîãëàñíîòåîðåìå Ýðáðàíà ñóùåñòâóåò êîíå÷íàÿ ïðîòèâîðå÷èâàÿ ñèñòåìàS 0 îñíîâíûõ ïðèìåðîâ äèçúþíêòîâ èç S . Ïîýòîìó ìû1.
Âíà÷àëå ïîêàæåì, ÷òî èç ïðîòèâîðå÷èâîé ñèñòåìû îñíîâíûõïðèìåðîâ äèçúþíêòîâ S 0 ìîæíî ðåçîëþòèâíî âûâåñòè ïóñòîéäèçúþíêò .2. À çàòåì íà îñíîâå ýòîãî âûâîäà ïîñòðîèì ðåçîëþòèâíûéâûâîä ïóñòîãî äèçúþíêòà èç ñàìîé ñèñòåìû S .ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀËåììà îá îñíîâíûõ ïðèìåðàõ äèçúþíêòîâÅñëè S 0 êîíå÷íàÿ ïðîòèâîðå÷èâàÿ ñèñòåìà îñíîâíûõïðèìåðîâ äèçúþíêòîâ, òî èç S 0 ðåçîëþòèâíî âûâîäèì ïóñòîéäèçúþíêò .Äîêàçàòåëüñòâî ëåììû.Èíäóêöèåé ïî ÷èñëó N ðàçëè÷íûõ îñíîâíûõ àòîìîâ â ñèñòåìåäèçúþíêòîâ S 0.00Áàçèñ (N = 0). Ñèñòåìà S ïðîòèâîðå÷èâà. Çíà÷èò, S 6= ∅.Íî â S 0 íåò íè îäíîãî àòîìà.
Çíà÷èò, â S 0 ñîäåðæèòñÿ òîëüêîïóñòîé äèçúþíêò . È îí ðåçîëþòèâíî âûâîäèì èç S 0.ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììû.Èíäóêòèâíûé ïåðåõîä (N + 1 → N ). Ðàññìîòðèìïðîèçâîëüíûé îñíîâíîé àòîì A0, âõîäÿùèé â ñîñòàâäèçúþíêòîâ èç S 0, è ðàçîáüåì ñèñòåìó S 0 íà òðè ÷àñòè:1. S10 = {D : D ∈ S 0, D = Db1 ∨ A0};2. S20 = {D : D ∈ S 0, D = Db2 ∨ ¬A0}.3. S30 = {D : D ∈ S 0, A0 ∈/ D, ¬A0 ∈/ D};Ïîñòðîèì âñå ðåçîëüâåíòû ïî êîíòðàðíîé ïàðå A0, ¬A0b1 ∨ Db2 : D1 = Db1 ∨ A0 ∈ S 0 , D2 = Db2 ∨ ¬A0 ∈ S 0 }S00 = {D12è ïîêàæåì, ÷òî ìíîæåñòâî äèçúþíêòîâ S 00 = S00 ∪ S30ïðîòèâîðå÷èâî.ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî'ëåììû.'$'b1 ∨ A0D&&S01b2 ∨ ¬A0D%&$S02$'S0 $S03íåò ëèòåð A0, ¬A0%&%%ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî'ëåììû.'$'S01b1 ∨ A0D$S02b2 ∨ ¬A0DB$'S0 $S03íåò ëèòåð A0, ¬A0BB&%&%&%B&%BB'$00BS'$'$B0S03B S0BNb1 ∨ Db2Dðåçîëüâåíòû&&íåò ëèòåð A0, ¬A0%&%%ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììû.Ðàññìîòðèì ïðîèçâîëüíóþ èíòåðïðåòàöèþ I .Äëÿ îïðåäåëåííîñòè áóäåì ïîëàãàòü, ÷òî I |= A0(åñëè I |= ¬A0, òî ðàññóæäåíèÿ áóäóò àíàëîãè÷íû).Ïîêàæåì, ÷òî I 6|= S 00.Ò.
ê. S 0 ïðîòèâîðå÷èâàÿ ñèñòåìà, âåðíî I 6|= S10 ∪ S20 ∪ S30 .Ò. ê. I |= A0 è S10 = {D : D ∈ S 0, D = Db ∨ A0}, âåðíî I |= S10 .Çíà÷èò, I 6|= S20 ∪ S30 .Âîçìîæíû äâà âàðèàíòà.Âàðèàíò 1. I 6|= S30 .ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììû.Ðàññìîòðèì ïðîèçâîëüíóþ èíòåðïðåòàöèþ I .Äëÿ îïðåäåëåííîñòè áóäåì ïîëàãàòü, ÷òî I |= A0(åñëè I |= ¬A0, òî ðàññóæäåíèÿ áóäóò àíàëîãè÷íû).Ïîêàæåì, ÷òî I 6|= S 00.Ò. ê.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
