9. Резолютивный вывод. Корректность резолютивного вывода. Применение метода резолюций (В.А. Захаров - Лекции), страница 2
Описание файла
Файл "9. Резолютивный вывод. Корректность резолютивного вывода. Применение метода резолюций" внутри архива находится в папке "В.А. Захаров - Лекции". PDF-файл из архива "В.А. Захаров - Лекции", который расположен в категории "". Всё это находится в предмете "математическая логика и логическое программирование" из 7 семестр, которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст 2 страницы из PDF
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..
