Лекции 2-11. Математическая логика (до колка) (1161869), страница 9
Текст из файла (страница 9)
. . , 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Ñèñòåìàäèçúþíêòîâ¬ϕ?ÏÍÔϕ1?SϕÎòðèöàíèå-Ðåçîëþòèâíûé âûâîäïóñòîãî äèçúþíêòà èç ñèñòåìû 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.Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А.
ЗахаровЛекция 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 ), .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
