Лекции В.А. Захарова (1157993), страница 10
Текст из файла (страница 10)
& 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. Построение системы дизъюнктов.ϕ2Sϕ = {D1 , D2 , . . . , DN },ϕ общезначимая ⇐⇒ система дизъюнктов Sϕ противоречива.ЭРБРАНОВСКИЕ ИНТЕРПРЕТАЦИИСистема дизъюнктов S = {D1 , D2 , . . . , DN } противоречиватогда и только тогда, когдадля каждой интерпретации Iв системе S найдется такой дизъюнктDi = ∀x1 . . . ∀xn (L1i ∨ L2i ∨ · · · ∨ Lki i )и в предметной области DI найдется такой набор элементовd1 , . . .
, dn ,для которых имеют местоI 6|= L1i [d1 , . . . , dn ], I 6|= L2i [d1 , . . . , dn ], . . . , I 6|= Lki i [d1 , . . . , dn ].А можно ли сократить множество рассматриваемыхинтерпретаций?ЭРБРАНОВСКИЕ ИНТЕРПРЕТАЦИИЭрбрановские интерпретаций (H-интерпретации, названные такпо имени французского метематика Herbrand ) — этоспециальная разновидность интерпретаций, в основе которыхлежат свободные алгебры.Предметная область эрбрановских интерпретаций называетсяэрбрановским универсумом (H-универсумом).Определение H-универсумаПусть задана некоторая сигнатура σ = hConst, Func, Predi.Тогда эрбрановским универсумом σ называется множество∞Sтермов Hσ =Hi , гдеi=0i = 0 H0 =Const, если Const 6= ∅,{c}, если Const = ∅ (эрбрановская константа );i → i + 1 Hi+1 = Hi ∪ {f (k) (t1 , .
. . , tk ) : f (k) ∈ Func, t1 , . . . , tk ∈ Hi }.ЭРБРАНОВСКИЕ ИНТЕРПРЕТАЦИИЭрбрановский универсум — это множество всех термов,которые можно построить из констант и функциональныхсимволов заданной сигнатуры. Термы эрбрановскогоуниверсума не содержат переменных и называются основнымитермами .ПримерПусть Const = ∅, Func = {f (1) , g (2) }. Тогдаi = 0 H0 = {c} (эрбрановская константа, т.к. Const = ∅);i = 1 H1 = {c, f (c), g (c, c)};i = 2 H2 = {c, f (c), g (c, c),f (f (c)), f (g (c, c)), g (f (c), c), g (c, f (c)),g (f (c), f (c)), g (c, g (c, c)), g (g (c, c), c),g (g (c, c), g (c, c)), g (f (c), g (c, c)), g (g (c, c), f (c))};i = 3 и. т.
д.ЭРБРАНОВСКИЕ ИНТЕРПРЕТАЦИИОпределение H-интерпретацииЭрбрановская интерпретация IH = hHσ , Const H , Func H , Prediсигнатуры σ = hConst, Func, Predi состоит изIстандартной предметной области — эрбрановскогоуниверсума Hσ ;Iстандартной оценки констант: Const H (c) = c,т. е. значением каждого константного символа cявляется его собственное изображение;Iстандартной оценки функциональных символов:Func H (f (n) ) = f : f(t1 , t2 , . . . , tn ) = f (n) (t1 , t2 , . . . , tn ),т. е. каждый функциональный символ f играет рольконструктора термов эрбрановского универсума;Iпроизвольной оценки предикатных символов.Таким образом, разные H-интерпретации отличаются толькоистолкованием предикатных символов.ЭРБРАНОВСКИЕ ИНТЕРПРЕТАЦИИПреимущества эрбрановских интерпретаций.IНе нужно заботиться о выборе области интерпретации — увсех H-интерпретаций одна и та же предметная область —H-универсум.IНе нужно заботиться об оценке функциональных символов— у всех H-интерпретаций одна и та же стандартнаяоценка Const и Func.IИ, как будет показано, для проверки противоречивостисистем дизъюнктов достаточно ограничитьсярассмотрением H-интерпретаций.ЭРБРАНОВСКИЕ ИНТЕРПРЕТАЦИИТеорема о H-интерпретацияхСистема дизъюнктов S выполнима тогда и только тогда, когдаS имеет эрбрановскую модель, т.е.
выполнима хотя бы в однойH-интерпретации.Доказательство(⇐) Очевидно.(⇒) Пусть S = {D1 , . . . , DN }, и I = hDI , Const I , Func I , Pred I i— некоторая модель для S, т. е. для любого дизъюнктаDi = ∀x1 . . . ∀xn (L1i ∨ L2i ∨ · · · ∨ Lki i ) из S и для любогонабора элементов d1 , . . . , dn из DI имеет местоI |= (L1i ∨ L2i ∨ · · · ∨ Lki i )[d1 , . .
. , dn ].Покажем, что существует H-интерпретация JH , в которойвыполняется каждый дизъюнкт Di из S.ЭРБРАНОВСКИЕ ИНТЕРПРЕТАЦИИДоказательствоПусть σ — сигнатура системы дизъюнктов S. Рассмотримэрбрановский универсум Hσ и отображениеα : Hσ → DI ,которое каждому основному терму t ∈ Hσ сопоставляетэлемент α(t) = dt ∈ DI , равный значению терма t винтерпретации I .Оценку Pred H предикатных символов в H-интерпретации Jопределим так:для любого предикатного символа P и любого набора основныхтермов t1 , . . . , tm ∈ Hσ положимP H (t1 , .
. . , tm ) = true ⇐⇒ P I (α(t1 ), . . . , α(tm )) = true.Эта оценка однозначно определяет H-интерпретацию JHЭРБРАНОВСКИЕ ИНТЕРПРЕТАЦИИДоказательствоТогда для любого функционального символа f , предикатногосимвола P и любого набора основных термов t1 , . . . , tm ∈ Hσверноα(f (t1 , . . . , tm )) = f I (α(t1 ), . .
. , α(tm )),JH |= P[t1 , . . . , tm ] ⇐⇒ I |= P[α(t1 ), . . . , α(tm )]Отображение α — это гомоморфизм интерпретации JH винтерпретацию I .Значит, для любого дизъюнкта D 0 = ∀x1 . . . ∀xm (L1 ∨ · · · ∨ Lk )и любого набора основных термов t1 , . . . , tm ∈ Hσ верноJH |= (L1 ∨ · · · ∨ Lk )[t1 , . . .
, tm ]⇐⇒I |= (L1 ∨ · · · ∨ Lk )[α(t1 ), . . . , α(tm )]ЭРБРАНОВСКИЕ ИНТЕРПРЕТАЦИИДоказательствоИтак, для любого дизъюнктаDi = ∀x1 . . . ∀xn (L1i ∨ L2i ∨ · · · ∨ Lki i ) из S и любого набораосновных термов t1 , . . . , tn ∈ Hσ имеемJH |= (L1i ∨ L2i ∨ · · · ∨ Lki i )[t1 , . . .
, tn ]⇐⇒I |= (L1i ∨ L2i ∨ · · · ∨ Lki i )[α(t1 ), . . . , α(tn )].ПосколькуI |= (L1i ∨ L2i ∨ · · · ∨ Lki i )[α(t1 ), . . . , α(tn )],все дизъюнкты из S выполнимы в построенной эрбрановскойинтерпретации JH .ЭРБРАНОВСКИЕ ИНТЕРПРЕТАЦИИСледствиеСистема дизъюнктов S противоречива тогда и только тогда,когда S невыполнима ни в одной эрбрановской интерпретации.Значит, для проверки противоречивости систем дизъюнктовдостаточно исследовать только эрбрановские интерпретации.ЭРБРАНОВСКИЕ ИНТЕРПРЕТАЦИИКак задавать H-интерпретации?Эрбрановские интерпретации полностью определяются оценкойпредикатных символов. Значит, достаточно указать оценку всехпредикатных символов.Пусть P (m) ∈ Pred, и t1 , . .
. , tm ∈ Hσ — набор основных термов.Тогда формула P (m) (t1 , . . . , tm ) называется основным атомом .Множество всех основных атомов называется эрбрановскимбазисом и обозначается BH .Всякая H-интерпретация I задается подмножеством B Iистинных основных атомов:B I = {P (m) (t1 , . . .
, tm ) : I |= P (m) (t1 , . . . , tm ), {t1 , . . . , tm } ⊆ H}.ЭРБРАНОВСКИЕ ИНТЕРПРЕТАЦИИПримерыIB I = ∅ соответствует интерпретации I , в которой все Pтождественно ложны.I |= P (m) [t1 , . . . , tm ] ⇐⇒ P (m) (t1 , . . . , tm ) ∈ ∅.IB I = BH соответствует интерпретации I , в которой все Pтождественно истинны.IПересечение B I1 ∩ B I2 задает интерпретацию, в которойистинны те и только те отношения, которые истинны вобоих интерпретациях I1 и I2 .Значит, это очень удобный способ задания интерпретаций,позволяющий проводить над нимитеоретико-множественные операции.В дальнейшем все H-интерпретации мы будем ассоциировать сподмножествами эрбрановского базиса BH .ТЕОРЕМА ЭРБРАНАВернемся к системам дизъюнктовПусть имеется дизъюнкт D = ∀x1 .
. . ∀xm (L1 ∨ · · · ∨ Lk ) и наборосновных термов t1 , . . . , tm из эрбрановского универсума Hσ .Тогда дизъюнкт D 0 = (L1 ∨ · · · ∨ Lk ){x1 /t1 , . . . , xm /tm },полученный из D подстановкой основных термов t1 , . . . , tmвместо всех переменных дизъюнкта D называется основнымпримером дизъюнкта D.ПримерD = ∀x1 ∀x2 (¬R(x1 , x2 ) ∨ P(h(x1 ))) — дизъюнкт,D 0 = ¬R(g (c 0 ), c 00 ) ∨ P(h(g (c 0 ))) = D{x1 /g (c 0 ), x2 /c 00 } —основной пример.ТЕОРЕМА ЭРБРАНАСистема дизъюнктов S = {D1 , D2 , . .
. , DN } противоречива⇐⇒для каждой H-интерпретации I в S найдется такой дизъюнктDi = (L1i ∨ L2i ∨ · · · ∨ Lki i ) и такой набор основных термовt1 , . . . , tm , для которых имеют местоI 6|= (L1i ∨ L2i ∨ . . . Lki i )[t1 , . . . , tm ]⇐⇒для каждой H-интерпретации I существует основной примерD 0 = Di {x1 /t1 , .
. . , xm /tm } дизъюнкта из системы S, длякоторогоI 6|= D 0 .ТЕОРЕМА ЭРБРАНАРассмотрим множество основных примеров дизъюнктовGS= {D 0 : D 0 — основной пример дизъюнкта из S,существует эрбрановская интерпретация I ⊆ BH :I 6|= D 0 }.Тогда система дизъюнктов S противоречива⇐⇒система основных примеров GS противоречива.ТЕОРЕМА ЭРБРАНАВспомним теорему компактности МальцеваМножество замкнутых формул T имеет модель тогда и толькотогда, когда каждое конечное подмножество T 0 , T 0 ⊆ T ,имеет модель.Таким образом, множество основных примеров дизъюнктов GSпротиворечиво⇐⇒существует конечное противоречивое подмножество G 0 ,G 0 ⊆ GS .И в результате проведенных рассуждений мы приходим кТеореме Эрбрана.ТЕОРЕМА ЭРБРАНАТеорема ЭрбранаСистема дизъюнктов S = {D1 , . .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
