586 слайдов лекций, страница 13
Описание файла
PDF-файл из архива "586 слайдов лекций", который расположен в категории "". Всё это находится в предмете "математическая логика и логическое программирование" из 7 семестр, которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст 13 страницы из PDF
. . , 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.Îñíîâûìàòåìàòè÷åñêîéëîãèêèèëîãè÷åñêîãîïðîãðàììèðîâàíèÿËÅÊÒÎÐ: Â.À.