Вопрос 3. Логика 1-го порядка. Выполнимость и общезначимость. Общая схема метода резолюций. (1161605), страница 2
Текст из файла (страница 2)
Сведение проблемы общезначимости к проблемепротиворечивости.ϕϕ0 = ¬ϕϕ общезначима ⇐⇒ ϕ0 противоречива.Этап 2. Построение предваренной нормальной формы (ПНФ).ϕ0ϕ1 = Q1 x1 Q2 x2 . . . Qn xn (D1 &D2 & . . . &DN )ϕ0 равносильна ϕ1 , т. е. I |= ϕ0 ⇔ I |= ϕ1 .ОБЩАЯ СХЕМА МЕТОДА РЕЗОЛЮЦИЙЭтап 3. Построение сколемовской стандартной формы (ССФ).ϕ1ϕ2 = ∀xi1 ∀xi2 . . . ∀xik (D1 &D2 & .
. . &DN )ϕ1 противоречива ⇐⇒ ϕ2 противоречива.Этап 4. Построение системы дизъюнктов.ϕ2Sϕ = {D1 , D2 , . . . , DN },где Di = Li1 ∨ Li2 ∨ · · · ∨ Limi .ϕ2 противоречива ⇐⇒ система дизъюнктов Sϕ противоречива.ОБЩАЯ СХЕМА МЕТОДА РЕЗОЛЮЦИЙЭтап 5. Резолютивный вывод тождественно ложного(противоречивого) дизъюнкта из системы Sϕ .Правило резолюции Res :D1 = D10 ∨ L, D2 = D20 ∨ ¬L.D0 = D10 ∨ D20Дизъюнкт D0 называется резольвентой дизъюнктов D1 и D2 .Резольвенты строят, пока не будет получен пустой дизъюнкт .Это возможно в случае D1 = L, D2 = ¬L:D1 = L, D2 = ¬LD0 = Система дизъюнктов Sϕ противоречива ⇔ из Sϕ резолютивновыводим пустой дизъюнкт .ИТОГ.
Формула ϕ общезначима ⇔ из системы дизъюнктов Sϕрезолютивно выводим пустой дизъюнкт .ОБЩАЯ СХЕМА МЕТОДА РЕЗОЛЮЦИЙИсходнаяформулаϕ-Отрицание¬ϕ?ССФϕ2?СистемадизъюнктовSϕПНФϕ1Резолютивный вывод- пустого дизъюнкта из системы SϕРАВНОСИЛЬНЫЕ ФОРМУЛЫВведем вспомогательную логическую связку эквиваленции ≡.Выражение ϕ ≡ ψ — это сокращенная запись формулы(ϕ → ψ)&(ψ → ϕ).ОпределениеФормулы ϕ и ψ будем называть равносильными , еслиформула ϕ ≡ ψ общезначима, т.
е. |= (ϕ → ψ)&(ψ → ϕ).Запись ϕ[ψ] означает, что формула ϕ содержит подформулу ψ.Запись ϕ[ψ/χ] обозначает формулу, которая образуется изформулы ϕ заменой некоторых (не обязательно всех)вхождений подформулы ψ на формулу χ.Теорема|= ψ ≡ χ=⇒ |= ϕ[ψ] ≡ ϕ[ψ/χ]ПРЕДВАРЕННЫЕ НОРМАЛЬНЫЕ ФОРМЫЗамкнутая формула ϕ называется предваренной нормальнойформой (ПНФ) , еслиϕ = Q1 x1 Q2 x2 .
. . Qn xn M(x1 , x2 , . . . , xn ),гдеIQ1 x1 Q2 x2 . . . Qn xn — кванторная приставка , соcтоящаяиз кванторов Q1 , Q2 , . . . , Qn ,IM(x1 , x2 , . . . , xn ) — матрица — бескванторнаяконъюнктивная нормальная форма (КНФ), т. е.M(x1 , x2 , . . . , xn ) = D1 & D2 & . . .
& DN ,где Di = Li1 ∨ Li2 ∨ · · · ∨ Liki — дизъюнкты , состоящие излитер Lij = Aij или Lij = ¬Aij , где Aij — атомарнаяформула.Теорема о ПНФДля любой замкнутой формулы ϕ существуетравносильная предваренная нормальная форма ψ.СКОЛЕМОВСКИЕ СТАНДАРТНЫЕ ФОРМЫПредваренная нормальная форма видаϕ = ∀xi1 ∀xi2 .
. . ∀xim M(xi1 , xi2 , . . . , xim ),в которой кванторная приставка не содержит кванторов ∃,называется сколемовской стандартной формой (ССФ) .Теорема о ССФДля любой замкнутой формулы ϕ существует такаясколемовская стандартная форма ψ, чтоϕ выполнима⇐⇒ψ выполнима.СИСТЕМЫ ДИЗЪЮНКТОВУтверждение|= ∀x (ϕ & ψ) ≡ ∀x ϕ & ∀xψИначе говоря, кванторы ∀ можно равномерно распределить посомножителям (дизъюнктам) КНФ.ТеоремаСколемовская стандартная формаϕ = ∀x1 ∀x2 .
. . ∀xm (D1 & D2 & . . . & DN )невыполнима тогда и только тогда, когда множество формулSϕ = {∀x1 ∀x2 . . . ∀xm D1 , ∀x1 ∀x2 . . . ∀xm D2 , . . . , ∀x1 ∀x2 . . . ∀xm DN }не имеет модели.СИСТЕМЫ ДИЗЪЮНКТОВКаждая формула множества Sϕ имеет вид∀x1 ∀x2 . . . ∀xm (L1 ∨ L2 ∨ · · · ∨ Lk )и называется дизъюнктом .В дальнейшем (по умолчанию) будем полагать, что всепеременные дизъюнкта связаны кванторами ∀, и кванторнуюприставку выписывать не будем.Каждый дизъюнкт состоит из литер L1 , L2 , . .
. , Lk . Литера —это либо атом, либо отрицание атома.Особо выделен дизъюнкт, в котором нет ни одной литеры.Такой дизъюнкт называется пустым дизъюнктом иобозначается . Пустой дизъюнкт тождественно ложен.СИСТЕМЫ ДИЗЪЮНКТОВСистему дизъюнктов, не имеющую моделей, будем называтьневыполнимой , или противоречивой системой дизъюнктов.Задача проверки общезначимости формул логики предикатов.|= ϕ ?ϕ общезначима ⇐⇒ ϕ0 = ¬ϕ невыполнима.ϕ0 невыполнима ⇐⇒ ПНФ ϕ1 невыполнима.ϕ1 невыполнима ⇐⇒ ССФ ϕ2 невыполнима.ϕ2 невыполнима ⇐⇒ система дизъюнктов Sϕ невыполнима.Итак, проверка общезначимости |= ϕ ? сводится к проверкепротиворечивости системы дизъюнктов Sϕ .РЕЗОЛЮТИВНЫЙ ВЫВОДО терминологии.Пусть задано выражение E и подстановка θ.Подстановка θ : Var → Var называется переименованием ,если θ — биекция.Если θ — переименование, то пример E θ называется вариантомвыражения E .Подстановка θ называется унификатором выражений E1 и E2 ,если E1 θ = E2 θ.Подстановка θ называется наиболее общим унификатором(НОУ) выражений E1 и E2 , если1.
θ — унификатор выражений E1 и E2 ;2. для любого унификатора η выражений E1 и E2 существуеттакая подстановка ρ, для которой верно равенствоη = θρРЕЗОЛЮТИВНЫЙ ВЫВОДПравило резолюции.Пусть D1 = D10 ∨ L1 и D2 = D20 ∨ ¬L2 — два дизъюнкта.Пусть θ ∈ НОУ(L1 , L2 ).Тогда дизъюнкт D0 = (D10 ∨ D20 )θ называется резольвентойдизъюнктов D1 и D2 .Пара литер L1 и ¬L2 называется контрарной парой .Правило резолюцииD10 ∨ L1 , D20 ∨ ¬L2,(D10 ∨ D20 )θθ ∈ НОУ(L1 , L2 )РЕЗОЛЮТИВНЫЙ ВЫВОДПравило склейки.Пусть D1 = D10 ∨ L1 ∨ L2 — дизъюнкт.Пусть η ∈ НОУ(L1 , L2 ).Тогда дизъюнкт D0 = (D10 ∨ L1 )η называется склейкойдизъюнкта D1 .Пара литер L1 и L2 называется склеиваемой парой .Правило склейкиD10 ∨ L1 ∨ L2,(D10 ∨ L1 )ηη ∈ НОУ(L1 , L2 )РЕЗОЛЮТИВНЫЙ ВЫВОДОпределение резолютивного вывода.Пусть S = {D1 , D2 , .
. . , 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 противоречива и опровергнуто предположениео ее выполнимости!Теорема корректности резолютивного выводаЕсли из системы дизъюнктов S резолютивно выводим пустойдизъюнкт , то S — противоречивая система дизъюнктов.Теорема о полноте резолютивного выводаЕсли S — противоречивая система дизъюнктов, то из Sрезолютивно выводим пустой дизъюнкт .ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙПример.Рассмотрим формулу ϕ∀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 ), (вариант D1 )2. D20 = A(g (y20 , u2 ), u2 ) ∨ A(z2 , f (y20 )), (вариант D2 )3. D30 = A(g (y30 , f (y30 )), f (y30 )), (склейка D20 )4. D40 = B(y40 , g (y40 , f (y40 ))), (резольвента D10 и D30 )5. D50 = ¬B(c, y500 ), (вариант D3 )6. D60 = . (резольвента D40 и D50 )ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешениеЗаключение. Успешный резолютивный вывод из Sϕ означает,что Sϕ — противоречивая система дизъюнктов.Значит, ϕ1 = ¬ϕ — невыполнимая формула.Значит, ϕ — общезначимая формула,|= ϕ.КОНЕЦ ОТВЕТА НА БИЛЕТ 1..
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
