Ещё одни лекции В.А. Захарова, страница 10

. . , 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 = Hσ , Const H , Func H , Predсигнатуры σ = Const, Func, Pred состоит изстандартной предметной области — эрбрановскогоуниверсума Hσ ;стандартной оценки констант: Const H (c) = c,т. е.

значением каждого константного символа cявляется его собственное изображение;стандартной оценки функциональных символов:Func H (f (n) ) = f : f(t1 , t2 , . . . , tn ) = f (n) (t1 , t2 , . . . , tn ),т. е. каждый функциональный символ f играет рольконструктора термов эрбрановского универсума;произвольной оценки предикатных символов.Таким образом, разные H-интерпретации отличаются толькоистолкованием предикатных символов.ЭРБРАНОВСКИЕ ИНТЕРПРЕТАЦИИПреимущества эрбрановских интерпретаций.Не нужно заботиться о выборе области интерпретации — увсех H-интерпретаций одна и та же предметная область —H-универсум.Не нужно заботиться об оценке функциональных символов— у всех H-интерпретаций одна и та же стандартнаяоценка Const и Func.И, как будет показано, для проверки противоречивостисистем дизъюнктов достаточно ограничитьсярассмотрением H-интерпретаций.ЭРБРАНОВСКИЕ ИНТЕРПРЕТАЦИИТеорема о H-интерпретацияхСистема дизъюнктов S выполнима тогда и только тогда, когдаS имеет эрбрановскую модель, т.е.

выполнима хотя бы в однойH-интерпретации.Доказательство(⇐) Очевидно.(⇒) Пусть S = {D1 , . . . , DN }, и I = DI , Const I , Func I , Pred 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 = ∀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}.ЭРБРАНОВСКИЕ ИНТЕРПРЕТАЦИИПримерыB I = ∅ соответствует интерпретации I , в которой все Pтождественно ложны.I |= P (m) [t1 , . . . , tm ] ⇐⇒ P (m) (t1 , . . . , tm ) ∈ ∅.B I = BH соответствует интерпретации I , в которой все Pтождественно истинны.Пересечение B I1 ∩ B I2 задает интерпретацию, в которойистинны те и только те отношения, которые истинны вобоих интерпретациях I1 и I2 .Значит, это очень удобный способ задания интерпретаций,позволяющий проводить над нимитеоретико-множественные операции.В дальнейшем все H-интерпретации мы будем ассоциировать сподмножествами эрбрановского базиса BH .ТЕОРЕМА ЭРБРАНАВернемся к системам дизъюнктовПусть имеется дизъюнкт D = ∀x1 .

. . ∀xm (L1 ∨ · · · ∨ Lk ) и наборосновных термов t1 , . . . , tm из эрбрановского универсума Hσ .Тогда дизъюнкт D = (L1 ∨ · · · ∨ Lk ){x1 /t1 , . . . , xm /tm },полученный из D подстановкой основных термов t1 , . . . , tmвместо всех переменных дизъюнкта D называется основнымпримером дизъюнкта D.ПримерD = ∀x1 ∀x2 (¬R(x1 , x2 ) ∨ P(h(x1 ))) — дизъюнкт,D = ¬R(g (c ), c ) ∨ P(h(g (c ))) = D{x1 /g (c ), x2 /c } —основной пример.ТЕОРЕМА ЭРБРАНАСистема дизъюнктов S = {D1 , D2 , .

. . , DN } противоречива⇐⇒для каждой H-интерпретации I в S найдется такой дизъюнктDi = (L1i ∨ L2i ∨ · · · ∨ Lki i ) и такой набор основных термовt1 , . . . , tm , для которых имеют местоI |= (L1i ∨ L2i ∨ . . . Lki i )[t1 , . . . , tm ]⇐⇒для каждой H-интерпретации I существует основной примерD = Di {x1 /t1 , . . .

, xm /tm } дизъюнкта из системы S, длякоторогоI |= D .ТЕОРЕМА ЭРБРАНАРассмотрим множество основных примеров дизъюнктовGS= {D : D — основной пример дизъюнкта из S,существует эрбрановская интерпретация I ⊆ BH :I |= D }.Тогда система дизъюнктов S противоречива⇐⇒система основных примеров GS противоречива.ТЕОРЕМА ЭРБРАНАВспомним теорему компактности МальцеваМножество замкнутых формул T имеет модель тогда и толькотогда, когда каждое конечное подмножество T , T ⊆ T ,имеет модель.Таким образом, множество основных примеров дизъюнктов GSпротиворечиво⇐⇒существует конечное противоречивое подмножество G ,G ⊆ GS .И в результате проведенных рассуждений мы приходим кТеореме Эрбрана.ТЕОРЕМА ЭРБРАНАТеорема ЭрбранаСистема дизъюнктов S = {D1 , .

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

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

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

Приведение выражений к общему виду называетсяунификацией .Нам нужен алгоритм унификации!ЗАДАЧА УНИФИКАЦИИПриведение двух атомов A и A к общему виду достигаетсяприменением такой подстановки θ, для которой A θ = A θ.Значит, для решения задачи унификации придется изучитьалгебраические свойства подстановок.ВоспоминанияПодстановка — это отображение θ : Var → Term.Конечная подстановка θ = {x1 /t1 , x2 /t2 , . . . , xn /tn }.E θ — применение подстановки θ к выражению E .ЗАДАЧА УНИФИКАЦИИКомпозиция подстановокПусть θ, η ∈ Subst. Композиция подстановок θη — этоподстановка μ, которая определяется следующимсоотношением:μ(x) = (xθ)η для любой x ∈ Var .УтверждениеПусть θ = {x1 /t1 , . . .

, xn /tn }, η = {y1 /s1 , . . . , ym /sm }. Тогдаподстановкаμ = {x1 /t1 η, . . . , xn /tn η} ∪{yi /si : yi ∈/ {x1 , x2 , . . . , xn }} −{xj /tj η : xj = tj η}.является композицией θη.ЗАДАЧА УНИФИКАЦИИДоказательствоμ = {x1 /t1 η, . . . , xn /tn η} ∪{yi /si : yi ∈/ {x1 , x2 , . . . , xn }} −{xj /tj η : xj = tj η}.Рассмотрим произвольную z ∈ Var . Возможны 3 варианта.1. z = xj ∈ Domθ . Тогда z(θη) = (xj θ)η = tj η.Если tj η = xj , то xj ∈ Domμ , и xj μ = tj η./ Domμ , и xj μ = xj .Если tj η = xj , то xj ∈В любом случае xi (θη) = xi μ.2. z = yi ∈ Domη \ Domθ . Тогда z(θη) = (yi θ)η = yi η = si ,и zμ = si ./ Domη ∪ Domθ .