Лекция 7. Эрбрановские интерпретации. Теорема Эрбрана. Задача унификации (1161878)
Текст из файла
Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А. ЗахаровЛекция 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 , .
Характеристики
Тип файла PDF
PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.
Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
