Лекции 2-11. Математическая логика (до колка) (1161869), страница 7
Текст из файла (страница 7)
. . , cin ).Если ϕ ∈ Γω , то P(ci1 , . . . , cin ) = true, и поэтому Iω |= ϕ.Если ψ ∈ ∆ω , то ψ 6∈ Γω (почему ? ).Значит, P(ci1 , . . . , cin ) = false, и поэтому Iω 6|= ψ.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАИндуктивный переходПредположим, что утверждение верно для всех формул,имеющих не более n связок и кванторов. Рассмотрим формулыϕ, ψ, содержащие n + 1 связку и квантор.Если ϕ = ϕ1 → ϕ2 ∈ Γω , то есть такая таблица Ti = hΓi |∆i i,что ϕ1 → ϕ2 ∈ Γi .Согласно описанию применяемой стратегии построениятабличного вывода, существует такая таблица Tj = hΓj |∆j i,j ≥ i, что ϕ1 → ϕ2 — первая формула в списке формул Γj .Поэтому либо ϕ1 ∈ ∆j+1 , либо ϕ2 ∈ Γj+1 .В первом случае, согласно индуктивному предполжению,Iω 6|= ϕ1 , и поэтому Iω |= ϕ.Во втором случае, согласно индуктивному предполжению,Iω |= ϕ2 , и поэтому Iω |= ϕ.Итак, в обоих случаях получаем Iω |= ϕ1 → ϕ2 .ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАИндуктивный переходАналогичные рассуждения применимы и для других связок.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАИндуктивный переходЕсли ϕ = ∀xϕ1 (x) ∈ Γω , то формула ∀xϕ1 (x) бесконечно частовстречается в левых частях таблиц Ti = hΓi |∆i i (почему ? ).Поэтому правило (L∀) применяется к формуле ∀xϕ1 (x)бесконечно часто.Тогда, согласно описанию применяемой стратегии построениятабличного вывода, для любой константы c, c ∈ Lω ,существует такая таблица Tj = hΓj |∆j i, что ϕ1 (c) ∈ Γj .Значит, согласно индуктивному предполжению, Iω |= ϕ1 (c) длялюбой константы c, c ∈ Lω .Так как DI = Lω , приходим к заключению о том, чтоIω |= ∀xϕ1 (x).ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАИндуктивный переходЕсли ϕ = ∀xϕ1 (x) ∈ ∆ω , то есть такая таблица Ti = hΓi |∆i i,что ∀xϕ1 (x) ∈ ∆i .Согласно описанию применяемой стратегии построениятабличного вывода, существует такая таблица Tj = hΓj |∆j i,j ≥ i, что ∀xϕ1 (x) — первая формула в списке формул ∆j .Поэтому существует такая константа c, c ∈ Lω , чтоϕ1 (c) ∈ ∆j+1 .Согласно индуктивному предполжению, это означает, чтоIω 6|= ϕ1 (c), и поэтому Iω 6|= ∀xϕ1 (x).Аналогичные рассуждения применимы и для формул сквантором ∃.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАТаким образом,любая формула ϕ, ϕ ∈ Γω , выполнима в интерпретации Iω ,любая формула ψ, ψ ∈ ∆ω , невыполнима в интерпретации Iω .Поскольку, Γ0 ⊆ Γω и ∆0 ⊆ ∆ω , приходим к заключению о том,чтоIω |= Γ0 , Iω 6|= ∆0 .Это означает, что таблица T0 выполнима в интерпретации Iωвопреки условию о невыполнимости T0 .Источник полученного противоречия — предположение оневозможности построить успешный вывод, руководствуясьописанной стратегией.
Значит, предложенная стратегияпозволяет построить успешный вывод для всякойневыполнимой таблицы.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАЭто было упрощенное доказательство теоремы полноты.А насколько существенны те упрощения, которые былиобъявлены в начале доказательства? А именно,IКакие изменения нужно внести в структуру данных,представляющих таблицы, чтобы доказательство можнобыло распространить и на таблицы, содержащиебесконечные множества формул?IКакие изменения нужно внести в стратегию построениятабличного вывода, чтобы построить успешный вывод дляневыполнимой таблицы, формулы которой содержатсложные термы?IКакие изменения нужно внести в определениеинтерпретации Iω , чтобы доказательство можно былоприменить к таблицам, содержащим незамкнутыеформулы?ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАТеорема Геделя (о полноте)Если формула ϕ общезначима, то существует успешныйтабличный вывод для таблицу Tϕ = h∅|ϕi.ДоказательствоСледует из теоремы полноты.Итак, формула ϕ общезначима⇐⇒для таблицы Tϕ существует успешный вывод.И в доказательстве теоремы полноты показано, как построитьэтот вывод.ТЕОРЕМА ЛЕВЕНГЕЙМА-СКОЛЕМАТеоремаФормула ϕ выполнима ⇐⇒ ϕ имеет модель сконечной или счетно-бесконечной предметной областью.ДоказательствоЕсли ϕ выполнима, то для таблицы Tϕ∗ = hϕ|∅i нельзяпостроить успешный вывод.
Применим стратегию издоказательства теоремы полноты. Т. к. Tϕ∗ выполнима,получим дерево с ветвью, в которой нет закрытых таблиц.Tϕ∗ = T0 −→ T1 −→ T2 −→ . . . −→ Tn −→ Tn+1 −→ . . .Для этой ветви построим интерпретацию Iω , в которойIDi = Lω = {c1 , c2 , . . . } — конечное или счетно-бесконечноемножество констант из таблиц последовательности;Iвыполнимы все таблицы Ti (в т.ч. и Tϕ∗ ).ТЕОРЕМА КОМПАКТНОСТИ МАЛЬЦЕВАТеоремаΓ |= ϕ ⇐⇒существует такое конечное подмножество Γ0 , Γ0 ⊆ Γ, что Γ0 |= ϕ.Доказательство1. Γ |= ϕ ⇐⇒ таблица T = hΓ|ϕi невыполнима (почему? )2. Таблица T = hΓ|ϕi невыполнима ⇐⇒ cуществуетуспешный вывод для T (почему? )3. успешный вывод — это конечное дерево, и поэтомусуществует лишь конечое множество формул Γ0 , Γ0 ⊆ Γ,к которым применяются правила вывода.4. Но тогда для таблицы T = hΓ0 |ϕi cуществует точно такойже успешный вывод.5.
Значит, Γ0 |= ϕ.АВТОМАТИЧЕСКОЕ ДОКАЗАТЕЛЬСТВОТЕОРЕМСтратегия построения табличного вывода, использованная вдоказательстве теоремы полноты — это алгоритм построениядоказательства истинности утверждений, выраженныхформулами логики предикатов.Автоматические системы построения доказательств(логических выводов) называются пруверами . От пруверовтребуются следующие качества:Iкорректность (абсолютно необходимо)Iполнота (очень-очень желательно)Iэффективность (желательно)Первый прувер (крайне неэффективный) был разработан в1957 в США (Newell, Simon, Show)АВТОМАТИЧЕСКОЕ ДОКАЗАТЕЛЬСТВОТЕОРЕМОбщая схема прувера'$'Формулы,Правилатаблицывывода,ϕ1'ϕknпрувера Π16%ΠNϕm-ϕ&ЯдроΠ2...-?&$%$&%АВТОМАТИЧЕСКОЕ ДОКАЗАТЕЛЬСТВОТЕОРЕМНаш прувер (табличный вывод) корректен и полон.
Нонасколько он эффективен?В алгоритме построения дерева табличного выводаприменяется двойной переборный поиск:Iвыбор формулы , к которой нужно применить правиловвода,Iвыбор правила , которое нужно применять к формуле.АВТОМАТИЧЕСКОЕ ДОКАЗАТЕЛЬСТВОТЕОРЕМВыбор формулыТрудно избежать перебора всех формул таблицы.База знанийВ огороде бузина.Растет(бузина, огород)ЗапросВ Киеве дядька.∃y (Дядька(y )&Живет(y , Киев))АВТОМАТИЧЕСКОЕ ДОКАЗАТЕЛЬСТВОТЕОРЕМВыбор формулыТрудно избежать перебора всех формул таблицы.База знанийВ огороде бузина.Растет(бузина, огород)Все в огороде посадил дядька.∀x(Растет(x, огород) →∃y (Посадил(y , x)&Дядька(y )));ЗапросВ Киеве дядька.∃y (Дядька(y )&Живет(y , Киев))АВТОМАТИЧЕСКОЕ ДОКАЗАТЕЛЬСТВОТЕОРЕМВыбор формулыТрудно избежать перебора всех формул таблицы.База знанийВ огороде бузина.Растет(бузина, огород)Все в огороде посадил дядька.∀x(Растет(x, огород) →∃y (Посадил(y , x)&Дядька(y )));Бузину посадил киевлянин.∀x(Посадил(x, бузина) →Живет(x, Киев));ЗапросВ Киеве дядька.∃y (Дядька(y )&Живет(y , Киев))АВТОМАТИЧЕСКОЕ ДОКАЗАТЕЛЬСТВОТЕОРЕМНаиболее критичный этап потроения табличного вывода —выбор нужного правила.
Это касается правил (L∀) и (R∃).L∀hΓ, ∀xϕ(x)|∆ihΓ, ∀xϕ(x), ϕ(x){x/t}|∆iR∃hΓ|∆, ∃xϕ(x)ihΓ|∆, ∃xϕ(x), ϕ(x){x/t}iпоскольку выбор терма t правилами не оговаривается. Простойперебор всех термов практически невозможен. (почему ? )АВТОМАТИЧЕСКОЕ ДОКАЗАТЕЛЬСТВОТЕОРЕМПотому что термов очень-очень много. Если есть одиндвухместный функциональный символ f (2) и две константыc1 , c2 , то с их помощью можно построить более 101000 основныхтермов высоты 10. Это количество значительно превосходитчисло наносекунд, прошедших с момента Большого Взрыва.Значит, нужно придумать способ, позволяющий быстро и точновычислять тот терм, который нужно подставлять вместопеременных, связанных кванторами.Эту задачу в 1964 г.
сумели решить Дж. Робинсон (методрезолюций) и С. Маслов (обратный метод ε-термов).КОНЕЦ ЛЕКЦИИ 5.Îñíîâûìàòåìàòè÷åñêîéëîãèêèèëîãè÷åñêîãîïðîãðàììèðîâàíèÿËÅÊÒÎÐ: Â.À. Çàõàðîâzakh@cs.msu.suhttp://mk.cs.msu.suËåêöèÿ 6.Îáùàÿ ñõåìà ìåòîäà ðåçîëþöèé.Ðàâíîñèëüíûå ôîðìóëû.Òåîðåìà î ðàâíîñèëüíîé çàìåíå.Ïðåäâàðåííàÿ íîðìàëüíàÿ ôîðìà.Ñêîëåìîâñêàÿ ñòàíäàðòíàÿ ôîðìà.Ñèñòåìû äèçúþíêòîâ.ÎÁÙÀß ÑÕÅÌÀ ÌÅÒÎÄÀ ÐÅÇÎËÞÖÈÉÇàäà÷à ïðîâåðêè îáùåçíà÷èìîñòè ôîðìóë ëîãèêè ïðåäèêàòîâ.|= ϕ ?Ýòàï 1. Ñâåäåíèå ïðîáëåìû îáùåçíà÷èìîñòè ê ïðîáëåìåïðîòèâîðå÷èâîñòè.ϕϕ0 = ¬ϕîáùåçíà÷èìà ⇐⇒ ϕ0 ïðîòèâîðå÷èâà.Ýòàï 2. Ïîñòðîåíèå ïðåäâàðåííîé íîðìàëüíîé ôîðìû (ÏÍÔ).ϕϕ0ϕ0ϕ1 = Q1 x1 Q2 x2 . . .
Qn xn (D1 &D2 & . . . &DN )ðàâíîñèëüíà ϕ1, ò. å. I |= ϕ0⇔ I |= ϕ1.ÎÁÙÀß ÑÕÅÌÀ ÌÅÒÎÄÀ ÐÅÇÎËÞÖÈÉÝòàï 3. Ïîñòðîåíèå ñêîëåìîâñêîé ñòàíäàðòíîé ôîðìû (ÑÑÔ).ϕ1ϕ2 = ∀xi1 ∀xi2 . . . ∀xik (D1 &D2 & . . . &DN )ïðîòèâîðå÷èâà ⇐⇒ ϕ2 ïðîòèâîðå÷èâà.Ýòàï 4. Ïîñòðîåíèå ñèñòåìû äèçúþíêòîâ.ϕ1ϕ2Sϕ = {D1 , D2 , . . . , DN },ãäå Di = Li1 ∨ Li2 ∨ · · · ∨ Lim .ϕ2 ïðîòèâîðå÷èâà ⇐⇒ ñèñòåìà äèçúþíêòîâ Sϕ ïðîòèâîðå÷èâà.iÎÁÙÀß ÑÕÅÌÀ ÌÅÒÎÄÀ ÐÅÇÎËÞÖÈÉÝòàï 5. Ðåçîëþòèâíûé âûâîä òîæäåñòâåííî ëîæíîãî(ïðîòèâîðå÷èâîãî) äèçúþíêòà èç ñèñòåìû Sϕ.00Ïðàâèëî ðåçîëþöèè Res : D1 = DD1 0∨=L,DD0 2∨=DD0 2 ∨ ¬L .12Äèçúþíêò D0 íàçûâàåòñÿ ðåçîëüâåíòîé äèçúþíêòîâ D1 è D2.Ðåçîëüâåíòû ñòðîÿò, ïîêà íå áóäåò ïîëó÷åí ïóñòîé äèçúþíêò .Ýòî âîçìîæíî â ñëó÷àå D1 = L, D2 = ¬L:D1 = L, D2 = ¬LD0 = Ñèñòåìà äèçúþíêòîâ Sϕ ïðîòèâîðå÷èâà ⇔ èç Sϕ ðåçîëþòèâíîâûâîäèì ïóñòîé äèçúþíêò .ÈÒÎÃ.
Ôîðìóëà ϕ îáùåçíà÷èìà ⇔ èç ñèñòåìû äèçúþíêòîâ Sϕðåçîëþòèâíî âûâîäèì ïóñòîé äèçúþíêò .ÎÁÙÀß ÑÕÅÌÀ ÌÅÒÎÄÀ ÐÅÇÎËÞÖÈÉÈñõîäíàÿôîðìóëà-ϕÑÑÔϕ2Ñèñòåìàäèçúþíêòîâ¬ϕ?ÏÍÔϕ1?SϕÎòðèöàíèå-Ðåçîëþòèâíûé âûâîäïóñòîãî äèçúþíêòà èç ñèñòåìû SϕÐÀÂÍÎÑÈËÜÍÛÅ ÔÎÐÌÓËÛÂâåäåì âñïîìîãàòåëüíóþ ëîãè÷åñêóþ ñâÿçêó ýêâèâàëåíöèè ≡.Âûðàæåíèå ϕ ≡ ψ ýòî ñîêðàùåííàÿ çàïèñü ôîðìóëû(ϕ → ψ)&(ψ → ϕ).ÎïðåäåëåíèåÔîðìóëû ϕ è ψ áóäåì íàçûâàòü ðàâíîñèëüíûìè , åñëèôîðìóëà ϕ ≡ ψ îáùåçíà÷èìà, ò.
å. |= (ϕ → ψ)&(ψ → ϕ).Óòâåðæäåíèå.1. Îòíîøåíèå ðàâíîñèëüíîñòè ýòî îòíîøåíèåýêâèâàëåíòíîñòè.2. Åñëè ôîðìóëà ϕ îáùåçíà÷èìà (âûïîëíèìà) è ðàâíîñèëüíàψ , òî ôîðìóëà ψ òàêæå îáùåçíà÷èìà (âûïîëíèìà), ò. å.|= ϕ è |= ϕ ≡ ψ =⇒ |= ψÐÀÂÍÎÑÈËÜÍÛÅ ÔÎÐÌÓËÛÏðèìåðû ðàâíîñèëüíûõ ôîðìóë1. Óäàëåíèå èìïëèêàöèè. |= ϕ → ψ ≡ ¬ϕ ∨ ψ,2. Ïåðåèìåíîâàíèåïåðåìåííûõ.|= ∀∃ x ϕ(x) ≡ ∀∃ y ϕ(y ),çäåñü ôîðìóëà ϕ(x) íå ñîäåðæèò ñâîáîäíûõ âõîæäåíèéïåðåìåííîé y , à ôîðìóëà ϕ(y ) íå ñîäåðæèò ñâîáîäíûõâõîæäåíèé ïåðåìåííîé x .3. Ïðîäâèæåíèå îòðèöàíèÿ.|= ¬¬ϕ ≡ ϕ,∨|= ¬(ϕ &∨ ψ) ≡ ¬ϕ & ¬ψ ,|= ¬ ∀∃ xϕ ≡ ∃∀ x¬ϕ,ÐÀÂÍÎÑÈËÜÍÛÅ ÔÎÐÌÓËÛÏðèìåðû ðàâíîñèëüíûõ ôîðìóë4. Âûíåñåíèåêâàíòîðîâ.∀∀|=|=∃ xϕ(x)&ψ∀∃ xϕ(x) ∨ ψ,≡ ∃ x(ϕ(x)&ψ)≡ ∀∃ x(ϕ(x) ∨ ψ)ψ,çäåñü ôîðìóëà íå ñîäåðæèò ñâîáîäíûõ âõîæäåíèéïåðåìåííîé x ,5. Çàêîíûáóëåâîé& àëãåáðû.|= ϕ &ψ≡ ψ ∨ ϕ,∨&&&|= ϕ ∨ (ψ ∨ χ) ≡ (ϕ &∨ ψ) ∨ χ,|= ϕ&(ψ ∨ χ) ≡ (ϕ&ψ) ∨ (ϕ&χ),|= ϕ ∨ (ψ&χ) ≡ (ϕ ∨ ψ)&(ϕ ∨ χ),|= ϕ &∨ ϕ ≡ ϕ,Äîêàçàòü ðàâíîñèëüíîñòü ìåòîäîì ñåìàíòè÷åñêèõ òàáëèö.ÒÅÎÐÅÌÀ Î ÐÀÂÍÎÑÈËÜÍÎÉ ÇÀÌÅÍÅÇàïèñü ϕ[ψ] îçíà÷àåò, ÷òî ôîðìóëà ϕ ñîäåðæèò ïîäôîðìóëó ψ.Çàïèñü ϕ[ψ/χ] îáîçíà÷àåò ôîðìóëó, êîòîðàÿ îáðàçóåòñÿ èçôîðìóëû ϕ çàìåíîé íåêîòîðûõ (íå îáÿçàòåëüíî âñåõ)âõîæäåíèé ïîäôîðìóëû ψ íà ôîðìóëó χ.Òåîðåìà|= ψ ≡ χÄîêàçàòåëüñòâî=⇒ |= ϕ[ψ] ≡ ϕ[ψ/χ]Èíäóêöèåé ïî ÷èñëó ñâÿçîê è êâàíòîðîâ â ôîðìóëå ϕÁàçèñ.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
