Лекции В.А. Захарова, страница 8

Применим стратегию издоказательства теоремы полноты. Т. к. 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. Çàêîíûáóëåâîé& àëãåáðû.|= ϕ &ψ≡ ψ ∨ ϕ,∨&&&|= ϕ ∨ (ψ ∨ χ) ≡ (ϕ &∨ ψ) ∨ χ,|= ϕ&(ψ ∨ χ) ≡ (ϕ&ψ) ∨ (ϕ&χ),|= ϕ ∨ (ψ&χ) ≡ (ϕ ∨ ψ)&(ϕ ∨ χ),|= ϕ &∨ ϕ ≡ ϕ,Äîêàçàòü ðàâíîñèëüíîñòü ìåòîäîì ñåìàíòè÷åñêèõ òàáëèö.ÒÅÎÐÅÌÀ Î ÐÀÂÍÎÑÈËÜÍÎÉ ÇÀÌÅÍÅÇàïèñü ϕ[ψ] îçíà÷àåò, ÷òî ôîðìóëà ϕ ñîäåðæèò ïîäôîðìóëó ψ.Çàïèñü ϕ[ψ/χ] îáîçíà÷àåò ôîðìóëó, êîòîðàÿ îáðàçóåòñÿ èçôîðìóëû ϕ çàìåíîé íåêîòîðûõ (íå îáÿçàòåëüíî âñåõ)âõîæäåíèé ïîäôîðìóëû ψ íà ôîðìóëó χ.Òåîðåìà|= ψ ≡ χÄîêàçàòåëüñòâî=⇒ |= ϕ[ψ] ≡ ϕ[ψ/χ]Èíäóêöèåé ïî ÷èñëó ñâÿçîê è êâàíòîðîâ â ôîðìóëå ϕÁàçèñ. ϕ[ψ] = ψ.

Î÷åâèäíî.ÒÅÎÐÅÌÀ Î ÐÀÂÍÎÑÈËÜÍÎÉ ÇÀÌÅÍÅÈíäóêòèâíûé ïåðåõîä. ϕ[ψ] = ∀xϕ1[ψ](x).Ïî èíäóêòèâíîìó ïðåäïîëîæåíèþ, åñëè |= ψ ≡ χ, òî â ëþáîéèíòåðïåðòàöèè I è äëÿ ëþáîãî ýëåìåíòà d ∈ DI âåðíîI |= ϕ1 [ψ](d) → ϕ1 [ψ/χ](d)I |= ϕ1 [ψ/χ](d) → ϕ1 [ψ](d)Çíà÷èò,I |= ∀x(ϕ1 [ψ](x) → ϕ1 [ψ/χ](x))I |= ∀x(ϕ1 [ψ/χ](x) → ϕ1 [ψ](x))Êàê ñëåäóåò èç ïðèìåðà |= ∀x(A → B) → (∀xA → ∀xB)(ñì. Ëåêöèÿ 3 ),I |= ∀xϕ1 [ψ](x) → ∀xϕ1 [ψ/χ](x))I |= ∀xϕ1 [ψ/χ](x) → ∀xϕ1 [ψ](x))(Îñòàëüíûå ñëó÷àè ôîðìóëû ϕ ñàìîñòîÿòåëüíî.)ÒÅÎÐÅÌÀ Î ÐÀÂÍÎÑÈËÜÍÎÉ ÇÀÌÅÍÅÐàâíîñèëüíûå çàìåíû ïîçâîëÿþò óïðîùàòü ôîðìóëû,ïîëíîñòüþ ñîõðàíÿÿ ïðè ýòîì èõ çíà÷åíèå (ñìûñë).ÒÅÎÐÅÌÀ Î ÐÀÂÍÎÑÈËÜÍÎÉ ÇÀÌÅÍÅÐàâíîñèëüíûå çàìåíû ïîçâîëÿþò óïðîùàòü ôîðìóëû,ïîëíîñòüþ ñîõðàíÿÿ ïðè ýòîì èõ çíà÷åíèå (ñìûñë).ÏðèìåðÄîêàçàòü îáùåçíà÷èìîñòü ôîðìóëû ∀xP(x) → ∃xP(x).ÒÅÎÐÅÌÀ Î ÐÀÂÍÎÑÈËÜÍÎÉ ÇÀÌÅÍÅÐàâíîñèëüíûå çàìåíû ïîçâîëÿþò óïðîùàòü ôîðìóëû,ïîëíîñòüþ ñîõðàíÿÿ ïðè ýòîì èõ çíà÷åíèå (ñìûñë).ÏðèìåðÄîêàçàòü îáùåçíà÷èìîñòü ôîðìóëû ∀xP(x) → ∃xP(x).|= ∀xP(x) → ∃xP(x) ≡ ¬∀xP(x) ∨ ∃xP(x)|= ϕ → ψ ≡ ¬ϕ ∨ ψÏîñêîëüêóÒÅÎÐÅÌÀ Î ÐÀÂÍÎÑÈËÜÍÎÉ ÇÀÌÅÍÅÐàâíîñèëüíûå çàìåíû ïîçâîëÿþò óïðîùàòü ôîðìóëû,ïîëíîñòüþ ñîõðàíÿÿ ïðè ýòîì èõ çíà÷åíèå (ñìûñë).ÏðèìåðÄîêàçàòü îáùåçíà÷èìîñòü ôîðìóëû ∀xP(x) → ∃xP(x).|= ∀xP(x) → ∃xP(x) ≡ ¬∀xP(x) ∨ ∃xP(x)|= ¬∀xP(x) ∨ ∃xP(x) ≡ ∃x¬P(x) ∨ ∃xP(x)|= ¬∀xϕ ≡ ∃x¬ϕÏîñêîëüêóÒÅÎÐÅÌÀ Î ÐÀÂÍÎÑÈËÜÍÎÉ ÇÀÌÅÍÅÐàâíîñèëüíûå çàìåíû ïîçâîëÿþò óïðîùàòü ôîðìóëû,ïîëíîñòüþ ñîõðàíÿÿ ïðè ýòîì èõ çíà÷åíèå (ñìûñë).ÏðèìåðÄîêàçàòü îáùåçíà÷èìîñòü ôîðìóëû ∀xP(x) → ∃xP(x).|= ∀xP(x) → ∃xP(x) ≡ ¬∀xP(x) ∨ ∃xP(x)|= ¬∀xP(x) ∨ ∃xP(x) ≡ ∃x¬P(x) ∨ ∃xP(x)|= ∃x¬P(x) ∨ ∃xP(x) ≡ ∃x¬P(x) ∨ ∃yP(y )|= ∃x ϕ(x) ≡ ∃y ϕ(y )ÏîñêîëüêóÒÅÎÐÅÌÀ Î ÐÀÂÍÎÑÈËÜÍÎÉ ÇÀÌÅÍÅÐàâíîñèëüíûå çàìåíû ïîçâîëÿþò óïðîùàòü ôîðìóëû,ïîëíîñòüþ ñîõðàíÿÿ ïðè ýòîì èõ çíà÷åíèå (ñìûñë).ÏðèìåðÄîêàçàòü îáùåçíà÷èìîñòü ôîðìóëû ∀xP(x) → ∃xP(x).|= ∀xP(x) → ∃xP(x) ≡ ¬∀xP(x) ∨ ∃xP(x)|= ¬∀xP(x) ∨ ∃xP(x) ≡ ∃x¬P(x) ∨ ∃xP(x)|= ∃x¬P(x) ∨ ∃xP(x) ≡ ∃x¬P(x) ∨ ∃yP(y )|= ∃x¬P(x) ∨ ∃yP(y ) ≡ ∃x∃y (¬P(x) ∨ P(y ))|= ∃xϕ(x) ∨ ψ ≡ ∃x(ϕ(x) ∨ ψ)ÏîñêîëüêóÒÅÎÐÅÌÀ Î ÐÀÂÍÎÑÈËÜÍÎÉ ÇÀÌÅÍÅÐàâíîñèëüíûå çàìåíû ïîçâîëÿþò óïðîùàòü ôîðìóëû,ïîëíîñòüþ ñîõðàíÿÿ ïðè ýòîì èõ çíà÷åíèå (ñìûñë).ÏðèìåðÄîêàçàòü îáùåçíà÷èìîñòü ôîðìóëû ∀xP(x) → ∃xP(x).|= ∀xP(x) → ∃xP(x) ≡ ¬∀xP(x) ∨ ∃xP(x)|= ¬∀xP(x) ∨ ∃xP(x) ≡ ∃x¬P(x) ∨ ∃xP(x)|= ∃x¬P(x) ∨ ∃xP(x) ≡ ∃x¬P(x) ∨ ∃yP(y )|= ∃x¬P(x) ∨ ∃yP(y ) ≡ ∃x∃y (¬P(x) ∨ P(y ))Òàêèì îáðàçîì, âîïðîñ îá îáùåçíà÷èìîñòè ∀xP(x) → ∃xP(x)ñâîäèòñÿ ê âîïðîñó îá îáùåçíà÷èìîñòè ∃x∃y (¬P(x) ∨ P(y ))ÏÐÅÄÂÀÐÅÍÍÛÅ ÍÎÐÌÀËÜÍÛÅ ÔÎÐÌÛÎïðåäåëåíèåÇàìêíóòàÿ ôîðìóëà ϕ íàçûâàåòñÿ ïðåäâàðåííîé íîðìàëüíîéôîðìîé (ÏÍÔ) , åñëèϕ = Q1 x1 Q2 x2 .

. . Qn xn M(x1 , x2 , . . . , xn ),ãäåIIQ1 x1 Q2 x2 . . . Qn xn êâàíòîðíàÿ ïðèñòàâêà , ñîcòîÿùàÿèç êâàíòîðîâ Q1, Q2, . . . , Qn ,M(x1 , x2 , . . . , xn ) ìàòðèöà áåñêâàíòîðíàÿêîíúþíêòèâíàÿ íîðìàëüíàÿ ôîðìà (ÊÍÔ), ò. å.M(x1 , x2 , . . . , xn ) = D1 & D2 & . .