Ещё одни лекции В.А. Захарова, страница 8

Значит, Γ |= ϕ.АВТОМАТИЧЕСКОЕ ДОКАЗАТЕЛЬСТВОТЕОРЕМСтратегия построения табличного вывода, использованная вдоказательстве теоремы полноты — это алгоритм построениядоказательства истинности утверждений, выраженныхформулами логики предикатов.Автоматические системы построения доказательств(логических выводов) называются пруверами . От пруверовтребуются следующие качества:корректность (абсолютно необходимо)полнота (очень-очень желательно)эффективность (желательно)Первый прувер (крайне неэффективный) был разработан в1957 в США (Newell, Simon, Show)АВТОМАТИЧЕСКОЕ ДОКАЗАТЕЛЬСТВОТЕОРЕМОбщая схема прувера$''Формулы,Правилатаблицывывода,ϕ1'-?ϕknЯдропрувера Π16Π2...%ΠNϕm-ϕ&&$%$&%АВТОМАТИЧЕСКОЕ ДОКАЗАТЕЛЬСТВОТЕОРЕМНаш прувер (табличный вывод) корректен и полон. Нонасколько он эффективен?В алгоритме построения дерева табличного выводаприменяется двойной переборный поиск:выбор формулы , к которой нужно применить правиловвода,выбор правила , которое нужно применять к формуле.АВТОМАТИЧЕСКОЕ ДОКАЗАТЕЛЬСТВОТЕОРЕМВыбор формулыТрудно избежать перебора всех формул таблицы.База знанийВ огороде бузина.Растет(бузина, огород)ЗапросВ Киеве дядька.∃y (Дядька(y )&Живет(y , Киев))АВТОМАТИЧЕСКОЕ ДОКАЗАТЕЛЬСТВОТЕОРЕМВыбор формулыТрудно избежать перебора всех формул таблицы.База знанийВ огороде бузина.Растет(бузина, огород)Все в огороде посадил дядька.∀x(Растет(x, огород) →∃y (Посадил(y , x)&Дядька(y )));ЗапросВ Киеве дядька.∃y (Дядька(y )&Живет(y , Киев))АВТОМАТИЧЕСКОЕ ДОКАЗАТЕЛЬСТВОТЕОРЕМВыбор формулыТрудно избежать перебора всех формул таблицы.База знанийВ огороде бузина.Растет(бузина, огород)Все в огороде посадил дядька.∀x(Растет(x, огород) →∃y (Посадил(y , x)&Дядька(y )));Бузину посадил киевлянин.∀x(Посадил(x, бузина) →Живет(x, Киев));ЗапросВ Киеве дядька.∃y (Дядька(y )&Живет(y , Киев))АВТОМАТИЧЕСКОЕ ДОКАЗАТЕЛЬСТВОТЕОРЕМНаиболее критичный этап потроения табличного вывода —выбор нужного правила.

Это касается правил (L∀) и (R∃).L∀Γ, ∀xϕ(x)|ΔΓ, ∀xϕ(x), ϕ(x){x/t}|ΔR∃Γ|Δ, ∃xϕ(x)Γ|Δ, ∃xϕ(x), ϕ(x){x/t}поскольку выбор терма t правилами не оговаривается. Простойперебор всех термов практически невозможен. (почему ? )АВТОМАТИЧЕСКОЕ ДОКАЗАТЕЛЬСТВОТЕОРЕМПотому что термов очень-очень много. Если есть одиндвухместный функциональный символ f (2) и две константыc1 , c2 , то с их помощью можно построить более 101000 основныхтермов высоты 10. Это количество значительно превосходитчисло наносекунд, прошедших с момента Большого Взрыва.Значит, нужно придумать способ, позволяющий быстро и точновычислять тот терм, который нужно подставлять вместопеременных, связанных кванторами.Эту задачу в 1964 г.

сумели решить Дж. Робинсон (методрезолюций) и С. Маслов (обратный метод ε-термов).КОНЕЦ ЛЕКЦИИ 5.Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А. Захаров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. Построение системы дизъюнктов.ϕ2 Sϕ = {D1 , D2 , . . . , DN },где Di = Li1 ∨ Li2 ∨ · · · ∨ Limi .ϕ2 противоречива ⇐⇒ система дизъюнктов Sϕ противоречива.ОБЩАЯ СХЕМА МЕТОДА РЕЗОЛЮЦИЙЭтап 5. Резолютивный вывод тождественно ложного(противоречивого) дизъюнкта из системы Sϕ .Правило резолюции Res :D1 = D1 ∨ L, D2 = D2 ∨ ¬L.D0 = D1 ∨ D2Дизъюнкт 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 ),гдеQ1 x1 Q2 x2 . . . Qn xn — кванторная приставка , соcтоящаяиз кванторов Q1 , Q2 , . . . , Qn ,M(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.