LectLog6 (Старые лекции, в целом тоже самое)

Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А. Захаров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 .