Ещё одни лекции В.А. Захарова (1158033), страница 9
Текст из файла (страница 9)
Вынесение кванторов «наружу».Применяем равносильности|= ∀∃ 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 ) )В результате получаем формулу ψ, котораяявляется предваренной нормальной формой,равносильна исходной формуле ϕ.ОБЩАЯ СХЕМА МЕТОДА РЕЗОЛЮЦИЙИсходнаяформулаϕ-Отрицание¬ϕ?ССФϕ2?СистемадизъюнктовSϕПНФϕ1Резолютивный вывод- пустого дизъюнкта из системы SϕСКОЛЕМОВСКИЕ СТАНДАРТНЫЕ ФОРМЫОпределениеПредваренная нормальная форма видаϕ = ∀xi1 ∀xi2 .
. . ∀xim M(xi1 , xi2 , . . . , xim ),в которой кванторная приставка не содержит кванторов ∃,называется сколемовской стандартной формой (ССФ) .Примеры ССФ∀x1 ∀y2 (P(x1 ) & (¬P(f (x1 )) ∨ R(x1 , g (x1 ))) & ¬R(x1 , y2 ) )R(c1 , f (c1 , c2 )) ∨ P(c2 )СКОЛЕМОВСКИЕ СТАНДАРТНЫЕ ФОРМЫТеорема о ССФДля любой замкнутой формулы ϕ существует такаясколемовская стандартная форма ψ, чтоϕ выполнима⇐⇒ψ выполнима.ДоказательствоВоспользуемся леммой об удалении кванторов существования .СКОЛЕМОВСКИЕ СТАНДАРТНЫЕ ФОРМЫЛемма об удалении кванторов существованияПусть ϕ = ∀x1 ∀x2 . . .
∀xk ∃xk+1 ϕ0 (x1 , x2 , . . . , xk , xk+1 ) —замкнутая формула, k ≥ 0, и k-местный функциональныйсимвол f (k) не содержится в формуле ϕ.Тогда формула ϕ выполнима в том и только том случае,когда выполнима формулаψ = ∀x1 ∀x2 . . . ∀xk ϕ0 (x1 , x2 , . . . , xk , f (k) (x1 , x2 , . . . , xk )).Доказательство леммы.(⇐ ) Пусть I — модель для ψ.Тогда для любого набора d1 , d2 , . . . , dk ∈ DI имеет местоI |= ϕ0 [d1 , d2 , . . . , dk , f (k) (d1 , d2 , . . .
, dk )],т. е. для любого набора d1 , d2 , . . . , dk ∈ DI существует такойэлемент dk+1 = f (k) (d1 , d2 , . . . , dk ), чтоI |= ϕ0 [d1 , d2 , . . . , dk , dk+1 ].Это означает, что I |= ∀x1 ∀x2 . . . ∀xk ∃xk+1 ϕ0 .СКОЛЕМОВСКИЕ СТАНДАРТНЫЕ ФОРМЫДоказательство леммы об удалении ∃.(⇒ ) Пусть I — модель для ϕ. Тогда для любого набораd1 , d2 , . .
. , dk ∈ DI существует такой элемент dk+1 ∈ DI , чтоI |= ϕ0 [d1 , d2 , . . . , dk , dk+1 ].Пусть f : DIk → DI — это некоторая функция, вычисляющаядля каждого набора d1 , d2 , . . . , dk ∈ DI такой элементdk+1 = f(d1 , d2 , . . . , dk ), чтоI |= ϕ0 [d1 , d2 , . . . , dk , dk+1 ].Рассмотрим интерпретацию I , которая отличается от I толькотем, что оценкой функционального символа f (k) являетсяфункция f.Тогда для любого набора d1 , d2 , . . . , dk верноI |= ϕ0 [d1 , d2 , .
. . , dk , f (k) (d1 , d2 , . . . , dk )]. (почему? )Это означает, чтоI |= ∀x1 ∀x2 . . . ∀xk ϕ0 (x1 , x2 , . . . , xk , f (k) (x1 , x2 , . . . , xk )).СКОЛЕМОВСКИЕ СТАНДАРТНЫЕ ФОРМЫПродолжение доказательства теоремы об ССФУдаляем по очереди кванторы существования с помощьюлеммы.ϕ = ∀x1 . . . ∀xk ∃xk+1 ∀xk+2 . . . ∀xm ∃xm+1 .
. .ϕ0 (x1 , . . . , xk , xk+1 , xk+2 . . . xm , xm+1 , . . . )ϕ = ∀x1 . . . ∀xk ∀xk+2 . . . ∀xm ∃xm+1 . . .ϕ0 (x1 , . . . , xk , f (x1 , . . . , xk ), xk+2 . . . xm , xm+1 , . . . )ϕ = ∀x1 . . . ∀xk ∀xk+2 . . . ∀xm . . .ϕ0 (x1 , . . . , xk , f (x1 , . . . , xk ), xk+2 . . . xm , g (x1 , . . . , xk , xk+2 , . . . , xm ), .
. . )и. т. д.При этом выполнимость формул сохраняется.СКОЛЕМОВСКИЕ СТАНДАРТНЫЕ ФОРМЫПримерϕ = ∀x1 ∃x2 ∃y1 ∀y2 (P(x1 ) & (¬P(x2 ) ∨ R(x1 , y1 )) & ¬R(x1 , y2 ) )СКОЛЕМОВСКИЕ СТАНДАРТНЫЕ ФОРМЫПримерϕ = ∀x1 ∃x2 ∃y1 ∀y2 (P(x1 ) & (¬P(x2 ) ∨ R(x1 , y1 )) & ¬R(x1 , y2 ) )ϕ = ∀x1 ∃y1 ∀y2 (P(x1 ) & (¬P(f (x1 )) ∨ R(x1 , y1 )) & ¬R(x1 , y2 ) )СКОЛЕМОВСКИЕ СТАНДАРТНЫЕ ФОРМЫПримерϕ = ∀x1 ∃x2 ∃y1 ∀y2 (P(x1 ) & (¬P(x2 ) ∨ R(x1 , y1 )) & ¬R(x1 , y2 ) )ϕ = ∀x1 ∃y1 ∀y2 (P(x1 ) & (¬P(f (x1 )) ∨ R(x1 , y1 )) & ¬R(x1 , y2 ) )ϕ = ∀x1 ∀y2 (P(x1 ) & (¬P(f (x1 )) ∨ R(x1 , g (x1 ))) & ¬R(x1 , y2 ) )ϕ выполнима⇐⇒ϕ выполнима.СКОЛЕМОВСКИЕ СТАНДАРТНЫЕ ФОРМЫТерм f (k) (x1 , .
. . , xk ), который подставляется вместо удаляемойпеременной xk+1 , связанной квантором ∃, называетсясколемовским термом .Если k = 0, то терм называется сколемовской константой .Процедура удаления кванторов ∃ называется сколемизацией .ОБЩАЯ СХЕМА МЕТОДА РЕЗОЛЮЦИЙИсходнаяформулаϕ-Отрицание¬ϕ?ССФϕ2?СистемадизъюнктовSϕПНФϕ1Резолютивный вывод- пустого дизъюнкта из системы SϕСИСТЕМЫ ДИЗЪЮНКТОВУтверждение|= ∀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 .Литера — это либо атом, либо отрицание атома.Особо выделен дизъюнкт, в котором нет ни одной литеры.Такой дизъюнкт называется пустым дизъюнктом иобозначается . Пустой дизъюнкт тождественно ложен(почему? ).Потому что |= L1 ∨ · · · ∨ Lk ≡ L1 ∨ · · · ∨ Lk ∨ false, и поэтомупри k = 0 имеем |= ≡ false.СИСТЕМЫ ДИЗЪЮНКТОВСистему дизъюнктов, не имеющую моделей, будем называтьневыполнимой , или противоречивой системой дизъюнктов.Задача проверки общезначимости формул логики предикатов.|= ϕ ?ϕ общезначима ⇐⇒ ϕ0 = ¬ϕ невыполнима.ϕ0 невыполнима ⇐⇒ ПНФ ϕ1 невыполнима.ϕ1 невыполнима ⇐⇒ ССФ ϕ2 невыполнима.ϕ2 невыполнима ⇐⇒ система дизъюнктов Sϕ невыполнима.Итак, проверка общезначимости |= ϕ ? сводится к проверкепротиворечивости системы дизъюнктов Sϕ .СИСТЕМЫ ДИЗЪЮНКТОВ: ПРИМЕРИсходная формула:ϕ = ∃x( (P(x) & (∀xP(x) → ∃yR(x, y ))) → ∃yR(x, y ) )Ее отрицание:ϕ0 = ¬ ∃x( (P(x) & (∀xP(x) → ∃yR(x, y ))) → ∃yR(x, y ) )Предваренная нормальная форма для ϕ0 :ϕ1 = ∀x1 ∃x2 ∃y1 ∀y2 (P(x1 ) & (¬P(x2 ) ∨ R(x1 , y1 )) & ¬R(x1 , y2 ) )Сколемовская стандартная форма:ϕ2 = ∀x1 ∀y2 (P(x1 ) & (¬P(f (x1 )) ∨ R(x1 , g (x1 ))) & ¬R(x1 , y2 ) )СИСТЕМЫ ДИЗЪЮНКТОВ: ПРИМЕРСистема дизъюнктов:Sϕ = {D1 = P(x1 ),D2 = ¬P(f (x1 )) ∨ R(x1 , g (x1 )),D3 = ¬R(x1 , y2 )}Задача:как проверить противоречивостьпроизвольной системыдизъюнктов?КОНЕЦ ЛЕКЦИИ 6.Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А.
ЗахаровЛекция 7.Эрбрановские интерпретации.Теорема Эрбрана.Задача унификации.ОБЩАЯ СХЕМА МЕТОДА РЕЗОЛЮЦИЙИсходнаяформулаϕ-Отрицание¬ϕ?ССФϕ2?СистемадизъюнктовSϕПНФϕ1Резолютивный вывод- пустого дизъюнкта из системы SϕЭРБРАНОВСКИЕ ИНТЕРПРЕТАЦИИПроверка общезначимости формулы ϕ сводится к проверкепротиворечивости системы дизъюнктов Sϕ .Этап 1. Сведение проблемы общезначимости к проблемепротиворечивости: ϕ ϕ0 = ¬ϕЭтап 2. Построение предваренной нормальной формы (ПНФ).ϕ0 ϕ1 = Q1 x1 Q2 x2 .
. . Qn xn (D1 &D2 & . . . &DN )Этап 3. Построение сколемовской стандартной формы (ССФ).ϕ1 ϕ2 = ∀xi1 ∀xi2 . . . ∀xik (D1 &D2 & . . . &DN )Этап 4. Построение системы дизъюнктов.ϕ2 Sϕ = {D1 , D2 , . . . , DN },ϕ общезначимая ⇐⇒ система дизъюнктов Sϕ противоречива.ЭРБРАНОВСКИЕ ИНТЕРПРЕТАЦИИСистема дизъюнктов S = {D1 , D2 , . . . , DN } противоречиватогда и только тогда, когдадля каждой интерпретации Iв системе S найдется такой дизъюнктDi = ∀x1 . . . ∀xn (L1i ∨ L2i ∨ · · · ∨ Lki i )и в предметной области DI найдется такой набор элементовd1 , .
. . , dn ,для которых имеют местоI |= L1i [d1 , . . . , dn ], I |= L2i [d1 , . . . , dn ], . . . , I |= Lki i [d1 , . . . , dn ].А можно ли сократить множество рассматриваемыхинтерпретаций?ЭРБРАНОВСКИЕ ИНТЕРПРЕТАЦИИЭрбрановские интерпретаций (H-интерпретации, названные такпо имени французского метематика Herbrand ) — этоспециальная разновидность интерпретаций, в основе которыхлежат свободные алгебры.Предметная область эрбрановских интерпретаций называетсяэрбрановским универсумом (H-универсумом).Определение H-универсумаПусть задана некоторая сигнатура σ = Const, Func, Pred.Тогда эрбрановским универсумом σ называется множество∞Hi , гдетермов Hσ =i = 0 H0 =i=0Const, если Const = ∅,{c}, если Const = ∅ (эрбрановская константа );i → i + 1 Hi+1 = Hi ∪ {f (k) (t1 , .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
