LectLog6 (1158001), страница 2

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

Текст из файла (страница 2)

. . ∀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 0 , которая отличается от I толькотем, что оценкой функционального символа f (k) являетсяфункция f.Тогда для любого набора d1 , d2 , . . .

, dk верноI 0 |= ϕ0 [d1 , d2 , . . . , dk , f (k) (d1 , d2 , . . . , dk )]. (почему? )Это означает, чтоI 0 |= ∀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 , . . . )ϕ0 = ∀x1 . . . ∀xk ∀xk+2 . . . ∀xm ∃xm+1 . . .ϕ0 (x1 , . . . , xk , f (x1 , . . . , xk ), xk+2 . . . xm , xm+1 , . . . )ϕ00 = ∀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 ) )ϕ0 = ∀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 ) )ϕ0 = ∀x1 ∃y1 ∀y2 (P(x1 ) & (¬P(f (x1 )) ∨ R(x1 , y1 )) & ¬R(x1 , y2 ) )ϕ00 = ∀x1 ∀y2 (P(x1 ) & (¬P(f (x1 )) ∨ R(x1 , g (x1 ))) & ¬R(x1 , y2 ) )ϕ выполнима⇐⇒ϕ00 выполнима.СКОЛЕМОВСКИЕ СТАНДАРТНЫЕ ФОРМЫТерм 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..

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

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