Главная » Все файлы » Просмотр файлов из архивов » PDF-файлы » 7. Эрбрановские интерпретации. Теорема Эрбрана. Задача унификации

7. Эрбрановские интерпретации. Теорема Эрбрана. Задача унификации (В.А. Захаров - Лекции)

Описание файла

Файл "7. Эрбрановские интерпретации. Теорема Эрбрана. Задача унификации" внутри архива находится в папке "В.А. Захаров - Лекции". PDF-файл из архива "В.А. Захаров - Лекции", который расположен в категории "лекции и семинары". Всё это находится в предмете "математическая логика и логическое программирование" из седьмого семестра, которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .

Просмотр PDF-файла онлайн

Текст из PDF

Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А. ЗахаровЛекция 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 , .

. . , DN } противоречива⇐⇒существует конечное противоречивое множество G 0основных примеров дизъюнктов системы S.В чем состоит главная особенность теоремы Эрбрана?Основной пример дизъюнкта не содержит предметныхпеременных, и поэтому является простой булевой формулойТаким образом проблема общезначимости формул логикипредикатов (сложная проблема!!!) сводится к проблемевыполнимости булевой формулы (простой проблеме??!!).ТЕОРЕМА ЭРБРАНАМаленькое лукавство.Увы, теорема Эрбрана не сообщает нам ничего о том, КАКИЕосновные примеры дизъюнктов образуют это противоречивоемножество G 0 .Нам нужно придумать механизм поиска этого противоречивогомножества G 0 .Дэвис и Патнем предложили использовать компьютер дляперебора всех эрбрановских интерпретаций в поискепротиворечивой системы основных примеров дизъюнктов. НоДж.

Робинсон поступил хитрее...Из дизъюнктов системы S нужно устранять потенциальныепротиворечия, пока не будут устранены все источникипротиворечия или не будет получено неустранимое (явное)противоречие.ТЕОРЕМА ЭРБРАНАЕсли в системе S содержатся дизъюнкты D1 = L и D2 = ¬L,то, очевидно, S противоречива (явное противоречие).А если в S есть дизъюнкты D1 = D10 ∨ L и D2 = D20 ∨ ¬L, тоI |= D1 и I |= D2 влечет I |= D10 ∨ D20 .

Значит, добавлениедизъюнкта D0 = D10 ∨ D20 к S не нарушает ее выполнимости.Зато устраняется потенциальное противоречие L и ¬L.Правило вывода, разрешающее противоречия,D10 ∨ L, D20 ∨ ¬LD10 ∨ D20называется правилом резолюции . Это правило можноприменять до тех пор, пока не возникнет неустранимоепротиворечие D1 = L и D2 = ¬L. Это и будет служитьпризнаком противоречивости системы S.ТЕОРЕМА ЭРБРАНАНу, а если D1 = P(x) и D2 = ¬P(f (y )), то как быть тогда?Ведь здесь нет явного противоречия.Противоречие здесь скрытое.

Свежие статьи
Популярно сейчас