LectLog6 (1158001)

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла

Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А. Захаровzakh@cs.msu.suhttp://mathcyb.cs.msu.su/courses/logprog.htmlЛекция 6.Общая схема метода резолюций.Равносильные формулы.Теорема о равносильной замене.Предваренная нормальная форма.Сколемовская стандартная форма.Системы дизъюнктов.ОБЩАЯ СХЕМА МЕТОДА РЕЗОЛЮЦИЙЗадача проверки общезначимости формул логики предикатов.|= ϕ ?Этап 1. Сведение проблемы общезначимости к проблемепротиворечивости.ϕϕ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ϕРАВНОСИЛЬНЫЕ ФОРМУЛЫВведем вспомогательную логическую связку эквиваленции ≡.Выражение ϕ ≡ ψ — это сокращенная запись формулы(ϕ → ψ)&(ψ → ϕ).ОпределениеФормулы ϕ и ψ будем называть равносильными , еслиформула ϕ ≡ ψ общезначима, т.

е. |= (ϕ → ψ)&(ψ → ϕ).Утверждение.1. Отношение равносильности — это отношениеэквивалентности.2. Если формула ϕ общезначима (выполнима) и равносильнаψ, то формула ψ также общезначима (выполнима), т. е.|= ϕ и |= ϕ ≡ ψ =⇒ |= ψРАВНОСИЛЬНЫЕ ФОРМУЛЫПримеры равносильных формул1. Удаление импликации. |= ϕ → ψ ≡ ¬ϕ ∨ ψ,2. Переименование переменных.|= ∀∃ x ϕ(x) ≡ ∀∃ y ϕ(y ),здесь формула ϕ(x) не содержит свободных вхожденийпеременной y , а формула ϕ(y ) не содержит свободныхвхождений переменной x.3. Продвижение отрицания.|= ¬¬ϕ ≡ ϕ,∨|= ¬(ϕ &∨ ψ) ≡ ¬ϕ & ¬ψ,|= ¬ ∀∃ xϕ ≡ ∃∀ x¬ϕ,РАВНОСИЛЬНЫЕ ФОРМУЛЫПримеры равносильных формул4. Вынесение кванторов.|= ∀∃ xϕ(x)&ψ ≡ ∀∃ x(ϕ(x)&ψ),|= ∀∃ xϕ(x) ∨ ψ ≡ ∀∃ x(ϕ(x) ∨ ψ),здесь формула ψ не содержит свободных вхожденийпеременной x,5.

Законы булевой алгебры.&|= ϕ &∨ ψ ≡ ψ ∨ ϕ,&&&|= ϕ &∨ (ψ ∨ χ) ≡ (ϕ ∨ ψ) ∨ χ,|= ϕ&(ψ ∨ χ) ≡ (ϕ&ψ) ∨ (ϕ&χ),|= ϕ ∨ (ψ&χ) ≡ (ϕ ∨ ψ)&(ϕ ∨ χ),|= ϕ &∨ ϕ ≡ ϕ,Доказать равносильность методом семантических таблиц.ТЕОРЕМА О РАВНОСИЛЬНОЙ ЗАМЕНЕЗапись ϕ[ψ] означает, что формула ϕ содержит подформулу ψ.Запись ϕ[ψ/χ] обозначает формулу, которая образуется изформулы ϕ заменой некоторых (не обязательно всех)вхождений подформулы ψ на формулу χ.Теорема|= ψ ≡ χ=⇒ |= ϕ[ψ] ≡ ϕ[ψ/χ]ДоказательствоИндукцией по числу связок и кванторов в формуле ϕБазис. ϕ[ψ] = ψ. Очевидно.ТЕОРЕМА О РАВНОСИЛЬНОЙ ЗАМЕНЕИндуктивный переход. ϕ[ψ] = ∀xϕ1 [ψ](x).По индуктивному предположению, если |= ψ ≡ χ, то в любойинтерпертации I и для любого элемента d ∈ DI верноI |= ϕ1 [ψ](d) → ϕ1 [ψ/χ](d)I |= ϕ1 [ψ/χ](d) → ϕ1 [ψ](d)Значит,I |= ∀x(ϕ1 [ψ](x) → ϕ1 [ψ/χ](x))I |= ∀x(ϕ1 [ψ/χ](x) → ϕ1 [ψ](x))Как следует из примера |= ∀x(A → B) → (∀xA → ∀xB)(см.

Лекция 3 ),I |= ∀xϕ1 [ψ](x) → ∀xϕ1 [ψ/χ](x))I |= ∀xϕ1 [ψ/χ](x) → ∀xϕ1 [ψ](x))(Остальные случаи формулы ϕ — самостоятельно.)ТЕОРЕМА О РАВНОСИЛЬНОЙ ЗАМЕНЕРавносильные замены позволяют упрощать формулы,полностью сохраняя при этом их значение (смысл).ТЕОРЕМА О РАВНОСИЛЬНОЙ ЗАМЕНЕРавносильные замены позволяют упрощать формулы,полностью сохраняя при этом их значение (смысл).ПримерДоказать общезначимость формулы ∀xP(x) → ∃xP(x).ТЕОРЕМА О РАВНОСИЛЬНОЙ ЗАМЕНЕРавносильные замены позволяют упрощать формулы,полностью сохраняя при этом их значение (смысл).ПримерДоказать общезначимость формулы ∀xP(x) → ∃xP(x).|= ∀xP(x) → ∃xP(x) ≡ ¬∀xP(x) ∨ ∃xP(x)Поскольку |= ϕ → ψ ≡ ¬ϕ ∨ ψТЕОРЕМА О РАВНОСИЛЬНОЙ ЗАМЕНЕРавносильные замены позволяют упрощать формулы,полностью сохраняя при этом их значение (смысл).ПримерДоказать общезначимость формулы ∀xP(x) → ∃xP(x).|= ∀xP(x) → ∃xP(x) ≡ ¬∀xP(x) ∨ ∃xP(x)|= ¬∀xP(x) ∨ ∃xP(x) ≡ ∃x¬P(x) ∨ ∃xP(x)Поскольку |= ¬∀xϕ ≡ ∃x¬ϕТЕОРЕМА О РАВНОСИЛЬНОЙ ЗАМЕНЕРавносильные замены позволяют упрощать формулы,полностью сохраняя при этом их значение (смысл).ПримерДоказать общезначимость формулы ∀xP(x) → ∃xP(x).|= ∀xP(x) → ∃xP(x) ≡ ¬∀xP(x) ∨ ∃xP(x)|= ¬∀xP(x) ∨ ∃xP(x) ≡ ∃x¬P(x) ∨ ∃xP(x)|= ∃x¬P(x) ∨ ∃xP(x) ≡ ∃x¬P(x) ∨ ∃yP(y )Поскольку |= ∃x ϕ(x) ≡ ∃y ϕ(y )ТЕОРЕМА О РАВНОСИЛЬНОЙ ЗАМЕНЕРавносильные замены позволяют упрощать формулы,полностью сохраняя при этом их значение (смысл).ПримерДоказать общезначимость формулы ∀xP(x) → ∃xP(x).|= ∀xP(x) → ∃xP(x) ≡ ¬∀xP(x) ∨ ∃xP(x)|= ¬∀xP(x) ∨ ∃xP(x) ≡ ∃x¬P(x) ∨ ∃xP(x)|= ∃x¬P(x) ∨ ∃xP(x) ≡ ∃x¬P(x) ∨ ∃yP(y )|= ∃x¬P(x) ∨ ∃yP(y ) ≡ ∃x∃y (¬P(x) ∨ P(y ))Поскольку |= ∃xϕ(x) ∨ ψ ≡ ∃x(ϕ(x) ∨ ψ)ТЕОРЕМА О РАВНОСИЛЬНОЙ ЗАМЕНЕРавносильные замены позволяют упрощать формулы,полностью сохраняя при этом их значение (смысл).ПримерДоказать общезначимость формулы ∀xP(x) → ∃xP(x).|= ∀xP(x) → ∃xP(x) ≡ ¬∀xP(x) ∨ ∃xP(x)|= ¬∀xP(x) ∨ ∃xP(x) ≡ ∃x¬P(x) ∨ ∃xP(x)|= ∃x¬P(x) ∨ ∃xP(x) ≡ ∃x¬P(x) ∨ ∃yP(y )|= ∃x¬P(x) ∨ ∃yP(y ) ≡ ∃x∃y (¬P(x) ∨ P(y ))Таким образом, вопрос об общезначимости ∀xP(x) → ∃xP(x)сводится к вопросу об общезначимости ∃x∃y (¬P(x) ∨ P(y ))ПРЕДВАРЕННЫЕ НОРМАЛЬНЫЕ ФОРМЫОпределениеЗамкнутая формула ϕ называется предваренной нормальнойформой (ПНФ) , еслиϕ = 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 — атомарнаяформула.ПРЕДВАРЕННЫЕ НОРМАЛЬНЫЕ ФОРМЫПример∀x∃y ∃z∀u (P(x) & ¬R(x, u) & (¬P(y ) ∨ R(x, z))),кванторная приставка:матрица:∀x∃y ∃z∀uP(x) & ¬R(x, u) & (¬P(y ) ∨ R(x, z))дизъюнкты: D1 = P(x),D2 = ¬R(x, u),D3 = ¬P(y ) ∨ R(x, z)ПРЕДВАРЕННЫЕ НОРМАЛЬНЫЕ ФОРМЫТеорема о ПНФДля любой замкнутой формулы ϕ существуетравносильная предваренная нормальная форма ψ.ДоказательствоЗамкнутую формулу ϕ можно привести к ПНФ применениемравносильных преобразований.

Покажем, как это надо делатьна примере формулыϕ = ¬ ∃x( (P(x) & (∀xP(x) → ∃yR(x, y ))) → ∃yR(x, y ) )ПРЕДВАРЕННЫЕ НОРМАЛЬНЫЕ ФОРМЫДоказательство1. Переименование переменных.Применяем равносильности |= ∀∃ x ϕ(x) ≡∀∃y ϕ(y )ϕ = ¬ ∃x( (P(x) & (∀xP(x) → ∃yR(x, y ))) → ∃yR(x, y ) )¬ ∃x1 ( (P(x1 ) & (∀x2 P(x2 ) → ∃yR(x1 , y))) → ∃yR(x1 , y) )¬ ∃x1 ( (P(x1 ) & (∀x2 P(x2 ) → ∃y1 R(x1 , y1 ))) → ∃y2 R(x1 , y2 ) )ПРЕДВАРЕННЫЕ НОРМАЛЬНЫЕ ФОРМЫДоказательство2.

Удаление импликаций.Применяем равносильность |= ϕ → ψ ≡ ¬ϕ ∨ ψПРЕДВАРЕННЫЕ НОРМАЛЬНЫЕ ФОРМЫДоказательство2. Удаление импликаций.¬ ∃x1 ( (P(x1 ) & (∀x2 P(x2 )→∃y1 R(x1 , y1 ))) → ∃y2 R(x1 , y2 ) )ПРЕДВАРЕННЫЕ НОРМАЛЬНЫЕ ФОРМЫДоказательство2. Удаление импликаций.¬ ∃x1 ( (P(x1 ) & (∀x2 P(x2 )→∃y1 R(x1 , y1 ))) → ∃y2 R(x1 , y2 ) )¬ ∃x1 ( ¬(P(x1 ) & (¬∀x2 P(x2 )∨∃y1 R(x1 , y1 ))) ∨ ∃y2 R(x1 , y2 ) )ПРЕДВАРЕННЫЕ НОРМАЛЬНЫЕ ФОРМЫДоказательство3. Продвижение отрицания вглубь.Применяем равносильности|= ¬¬ϕ ≡ ϕ,∨|= ¬(ϕ &∨ ψ) ≡ ¬ϕ & ¬ψ,|= ¬ ∀∃ xϕ ≡ ∃∀ x¬ϕПРЕДВАРЕННЫЕ НОРМАЛЬНЫЕ ФОРМЫДоказательство3. Продвижение отрицания вглубь.¬ ∃x1 ( ¬(P(x1 ) & (¬∀x2 P(x2 ) ∨ ∃y1 R(x1 , y1 ))) ∨ ∃y2 R(x1 , y2 ) )ПРЕДВАРЕННЫЕ НОРМАЛЬНЫЕ ФОРМЫДоказательство3.

Продвижение отрицания вглубь.¬ ∃x1 ( ¬(P(x1 ) & (¬∀x2 P(x2 ) ∨ ∃y1 R(x1 , y1 ))) ∨ ∃y2 R(x1 , y2 ) )∀x1 ¬( ¬(P(x1 ) & (¬∀x2 P(x2 ) ∨ ∃y1 R(x1 , y1 ))) ∨ ∃y2 R(x1 , y2 ) )ПРЕДВАРЕННЫЕ НОРМАЛЬНЫЕ ФОРМЫДоказательство3. Продвижение отрицания вглубь.¬ ∃x1 ( ¬(P(x1 ) & (¬∀x2 P(x2 ) ∨ ∃y1 R(x1 , y1 ))) ∨ ∃y2 R(x1 , y2 ) )∀x1 ¬( ¬(P(x1 ) & (¬∀x2 P(x2 ) ∨ ∃y1 R(x1 , y1 ))) ∨ ∃y2 R(x1 , y2 ) )∀x1 ( ¬¬(P(x1 ) & (¬∀x2 P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ¬∃y2 R(x1 , y2 ) )ПРЕДВАРЕННЫЕ НОРМАЛЬНЫЕ ФОРМЫДоказательство3.

Продвижение отрицания вглубь.¬ ∃x1 ( ¬(P(x1 ) & (¬∀x2 P(x2 ) ∨ ∃y1 R(x1 , y1 ))) ∨ ∃y2 R(x1 , y2 ) )∀x1 ¬( ¬(P(x1 ) & (¬∀x2 P(x2 ) ∨ ∃y1 R(x1 , y1 ))) ∨ ∃y2 R(x1 , y2 ) )∀x1 ( ¬¬(P(x1 ) & (¬∀x2 P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ¬∃y2 R(x1 , y2 ) )∀x1 ( (P(x1 ) & (¬∀x2 P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ∀y2 ¬R(x1 , y2 ) )ПРЕДВАРЕННЫЕ НОРМАЛЬНЫЕ ФОРМЫДоказательство3. Продвижение отрицания вглубь.¬ ∃x1 ( ¬(P(x1 ) & (¬∀x2 P(x2 ) ∨ ∃y1 R(x1 , y1 ))) ∨ ∃y2 R(x1 , y2 ) )∀x1 ¬( ¬(P(x1 ) & (¬∀x2 P(x2 ) ∨ ∃y1 R(x1 , y1 ))) ∨ ∃y2 R(x1 , y2 ) )∀x1 ( ¬¬(P(x1 ) & (¬∀x2 P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ¬∃y2 R(x1 , y2 ) )∀x1 ( (P(x1 ) & (¬∀x2 P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ∀y2 ¬R(x1 , y2 ) )∀x1 ( (P(x1 ) & (∃x2 ¬P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ∀y2 ¬R(x1 , y2 ) )ПРЕДВАРЕННЫЕ НОРМАЛЬНЫЕ ФОРМЫДоказательство4.

Вынесение кванторов «наружу».Применяем равносильности|= ∀∃ xϕ(x)&ψ ≡ ∀∃ x(ϕ(x)&ψ),|= ∀∃ xϕ(x) ∨ ψ ≡ ∀∃ x(ϕ(x) ∨ ψ),&|= ϕ &∨ ψ ≡ ψ ∨ ϕ.ПРЕДВАРЕННЫЕ НОРМАЛЬНЫЕ ФОРМЫДоказательство4. Вынесение кванторов «наружу».∀x1 ( (P(x1 ) & (∃x2 ¬P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ∀y2 ¬R(x1 , y2 ) )ПРЕДВАРЕННЫЕ НОРМАЛЬНЫЕ ФОРМЫДоказательство4. Вынесение кванторов «наружу».∀x1 ( (P(x1 ) & (∃x2 ¬P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ∀y2 ¬R(x1 , y2 ) )∀x1 ( (P(x1 ) & ∃x2 (¬P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ∀y2 ¬R(x1 , y2 ) )ПРЕДВАРЕННЫЕ НОРМАЛЬНЫЕ ФОРМЫДоказательство4.

Вынесение кванторов «наружу».∀x1 ( (P(x1 ) & (∃x2 ¬P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ∀y2 ¬R(x1 , y2 ) )∀x1 ( (P(x1 ) & ∃x2 (¬P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ∀y2 ¬R(x1 , y2 ) )∀x1 ( ∃x2 (P(x1 ) & (¬P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ∀y2 ¬R(x1 , y2 ) )ПРЕДВАРЕННЫЕ НОРМАЛЬНЫЕ ФОРМЫДоказательство4. Вынесение кванторов «наружу».∀x1 ( (P(x1 ) & (∃x2 ¬P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ∀y2 ¬R(x1 , y2 ) )∀x1 ( (P(x1 ) & ∃x2 (¬P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ∀y2 ¬R(x1 , y2 ) )∀x1 ( ∃x2 (P(x1 ) & (¬P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ∀y2 ¬R(x1 , y2 ) )∀x1 ∃x2 ( (P(x1 ) & (¬P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ∀y2 ¬R(x1 , y2 ) )и так далее...ПРЕДВАРЕННЫЕ НОРМАЛЬНЫЕ ФОРМЫДоказательство4. Вынесение кванторов «наружу».∀x1 ( (P(x1 ) & (∃x2 ¬P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ∀y2 ¬R(x1 , y2 ) )∀x1 ( (P(x1 ) & ∃x2 (¬P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ∀y2 ¬R(x1 , y2 ) )∀x1 ( ∃x2 (P(x1 ) & (¬P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ∀y2 ¬R(x1 , y2 ) )∀x1 ∃x2 ( (P(x1 ) & (¬P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ∀y2 ¬R(x1 , y2 ) )и так далее...∀x1 ∃x2 ∃y1 ∀y2 ( (P(x1 ) & (¬P(x2 ) ∨ R(x1 , y1 ))) & ¬R(x1 , y2 ) )ПРЕДВАРЕННЫЕ НОРМАЛЬНЫЕ ФОРМЫДоказательство5.

Приведение матрицы к конъюнктивной нормальной форме.Применяем законы булевой алгебры.ПРЕДВАРЕННЫЕ НОРМАЛЬНЫЕ ФОРМЫДоказательство5. Приведение матрицы к конъюнктивной нормальной форме.ψ = ∀x1 ∃x2 ∃y1 ∀y2 (P(x1 ) & (¬P(x2 ) ∨ R(x1 , y1 )) & ¬R(x1 , y2 ) )В результате получаем формулу ψ, котораяIявляется предваренной нормальной формой,Iравносильна исходной формуле ϕ.ОБЩАЯ СХЕМА МЕТОДА РЕЗОЛЮЦИЙИсходнаяформулаϕ-Отрицание¬ϕ?ССФϕ2?СистемадизъюнктовSϕПНФϕ1Резолютивный вывод- пустого дизъюнкта из системы SϕСКОЛЕМОВСКИЕ СТАНДАРТНЫЕ ФОРМЫОпределениеПредваренная нормальная форма видаϕ = ∀xi1 ∀xi2 .

Характеристики

Тип файла PDF

PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.

Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.

Список файлов лекций