586 слайдов лекций, страница 10

PDF-файл 586 слайдов лекций, страница 10 Математическая логика и логическое программирование (53282): Лекции - 7 семестр586 слайдов лекций: Математическая логика и логическое программирование - PDF, страница 10 (53282) - СтудИзба2019-09-18СтудИзба

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

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

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

Текст 10 страницы из PDF

. . , 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 ), . . . , α(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 , .

Свежие статьи
Популярно сейчас
Зачем заказывать выполнение своего задания, если оно уже было выполнено много много раз? Его можно просто купить или даже скачать бесплатно на СтудИзбе. Найдите нужный учебный материал у нас!
Ответы на популярные вопросы
Да! Наши авторы собирают и выкладывают те работы, которые сдаются в Вашем учебном заведении ежегодно и уже проверены преподавателями.
Да! У нас любой человек может выложить любую учебную работу и зарабатывать на её продажах! Но каждый учебный материал публикуется только после тщательной проверки администрацией.
Вернём деньги! А если быть более точными, то автору даётся немного времени на исправление, а если не исправит или выйдет время, то вернём деньги в полном объёме!
Да! На равне с готовыми студенческими работами у нас продаются услуги. Цены на услуги видны сразу, то есть Вам нужно только указать параметры и сразу можно оплачивать.
Отзывы студентов
Ставлю 10/10
Все нравится, очень удобный сайт, помогает в учебе. Кроме этого, можно заработать самому, выставляя готовые учебные материалы на продажу здесь. Рейтинги и отзывы на преподавателей очень помогают сориентироваться в начале нового семестра. Спасибо за такую функцию. Ставлю максимальную оценку.
Лучшая платформа для успешной сдачи сессии
Познакомился со СтудИзбой благодаря своему другу, очень нравится интерфейс, количество доступных файлов, цена, в общем, все прекрасно. Даже сам продаю какие-то свои работы.
Студизба ван лав ❤
Очень офигенный сайт для студентов. Много полезных учебных материалов. Пользуюсь студизбой с октября 2021 года. Серьёзных нареканий нет. Хотелось бы, что бы ввели подписочную модель и сделали материалы дешевле 300 рублей в рамках подписки бесплатными.
Отличный сайт
Лично меня всё устраивает - и покупка, и продажа; и цены, и возможность предпросмотра куска файла, и обилие бесплатных файлов (в подборках по авторам, читай, ВУЗам и факультетам). Есть определённые баги, но всё решаемо, да и администраторы реагируют в течение суток.
Маленький отзыв о большом помощнике!
Студизба спасает в те моменты, когда сроки горят, а работ накопилось достаточно. Довольно удобный сайт с простой навигацией и огромным количеством материалов.
Студ. Изба как крупнейший сборник работ для студентов
Тут дофига бывает всего полезного. Печально, что бывают предметы по которым даже одного бесплатного решения нет, но это скорее вопрос к студентам. В остальном всё здорово.
Спасательный островок
Если уже не успеваешь разобраться или застрял на каком-то задание поможет тебе быстро и недорого решить твою проблему.
Всё и так отлично
Всё очень удобно. Особенно круто, что есть система бонусов и можно выводить остатки денег. Очень много качественных бесплатных файлов.
Отзыв о системе "Студизба"
Отличная платформа для распространения работ, востребованных студентами. Хорошо налаженная и качественная работа сайта, огромная база заданий и аудитория.
Отличный помощник
Отличный сайт с кучей полезных файлов, позволяющий найти много методичек / учебников / отзывов о вузах и преподователях.
Отлично помогает студентам в любой момент для решения трудных и незамедлительных задач
Хотелось бы больше конкретной информации о преподавателях. А так в принципе хороший сайт, всегда им пользуюсь и ни разу не было желания прекратить. Хороший сайт для помощи студентам, удобный и приятный интерфейс. Из недостатков можно выделить только отсутствия небольшого количества файлов.
Спасибо за шикарный сайт
Великолепный сайт на котором студент за не большие деньги может найти помощь с дз, проектами курсовыми, лабораторными, а также узнать отзывы на преподавателей и бесплатно скачать пособия.
Популярные преподаватели
Нашёл ошибку?
Или хочешь предложить что-то улучшить на этой странице? Напиши об этом и получи бонус!
Бонус рассчитывается индивидуально в каждом случае и может быть в виде баллов или бесплатной услуги от студизбы.
Предложить исправление
Добавляйте материалы
и зарабатывайте!
Продажи идут автоматически
5076
Авторов
на СтудИзбе
455
Средний доход
с одного платного файла
Обучение Подробнее