Лекция 6. Общая схема метода резолюций. Равносильные формулы. Теорема о равносильной замене... (Лекции 2014)
Описание файла
Файл "Лекция 6. Общая схема метода резолюций. Равносильные формулы. Теорема о равносильной замене..." внутри архива находится в папке "Лекции 2014". PDF-файл из архива "Лекции 2014", который расположен в категории "". Всё это находится в предмете "математическая логика и логическое программирование" из 8 семестр, которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст из PDF
Îñíîâûìàòåìàòè÷åñêîéëîãèêèèëîãè÷åñêîãîïðîãðàììèðîâàíèÿËÅÊÒÎÐ: Â.À. Çàõàðîâ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 & . . . & DN ,ãäå Di = Li1 ∨ Li2 ∨ · · · ∨ Lik äèçúþíêòû , ñîñòîÿùèå èçëèòåð Lij = Aij èëè Lij = ¬Aij , ãäå Aij àòîìàðíàÿôîðìóëà.iÏÐÅÄÂÀÐÅÍÍÛÅ ÍÎÐÌÀËÜÍÛÅ ÔÎÐÌÛÏðèìåð∀x∃y ∃z∀u (P(x) & ¬R(x, u) & (¬P(y ) ∨ R(x, z))),êâàíòîðíàÿ ïðèñòàâêà: ∀x∃y ∃z∀uìàòðèöà: P(x) & ¬R(x, u) & (¬P(y )äèçúþíêòû: D1 = P(x),D2 = ¬R(x, u),D3 = ¬P(y ) ∨ R(x, z)∨ R(x, z))ÏÐÅÄÂÀÐÅÍÍÛÅ ÍÎÐÌÀËÜÍÛÅ ÔÎÐÌÛÒåîðåìà î ÏÍÔÄëÿ ëþáîé çàìêíóòîé ôîðìóëû ϕ ñóùåñòâóåòðàâíîñèëüíàÿ ïðåäâàðåííàÿ íîðìàëüíàÿ ôîðìà ψ.ÄîêàçàòåëüñòâîÇàìêíóòóþ ôîðìóëó ϕ ìîæíî ïðèâåñòè ê ÏÍÔ ïðèìåíåíèåìðàâíîñèëüíûõ ïðåîáðàçîâàíèé.
Ïîêàæåì, êàê ýòî íàäî äåëàòüíà ïðèìåðå ôîðìóëûϕ = ¬ ∃x( (P(x) & (∀xP(x) → ∃yR(x, y ))) → ∃yR(x, y ) )ÏÐÅÄÂÀÐÅÍÍÛÅ ÍÎÐÌÀËÜÍÛÅ ÔÎÐÌÛÄîêàçàòåëüñòâî1. Ïåðåèìåíîâàíèå ïåðåìåííûõ. ∀Ïðèìåíÿåì ðàâíîñèëüíîñòè |= ∃ x ϕ(x)≡∀∃y ϕ(y )ϕ = ¬ ∃x( (P(x) & (∀xP(x) → ∃yR(x, y ))) → ∃yR(x, y ) )¬ ∃x1 ( (P(x1 ) & (∀x2 P(x2 ) → ∃yR(x1 , y))) → ∃yR(x1 , y) )¬ ∃x1 ( (P(x1 ) & (∀x2 P(x2 ) → ∃y1 R(x1 , y1 ))) → ∃y2 R(x1 , y2 ) )ÏÐÅÄÂÀÐÅÍÍÛÅ ÍÎÐÌÀËÜÍÛÅ ÔÎÐÌÛÄîêàçàòåëüñòâî2. Óäàëåíèå èìïëèêàöèé.Ïðèìåíÿåì ðàâíîñèëüíîñòü |=ϕ → ψ ≡ ¬ϕ ∨ ψÏÐÅÄÂÀÐÅÍÍÛÅ ÍÎÐÌÀËÜÍÛÅ ÔÎÐÌÛÄîêàçàòåëüñòâî2.
Óäàëåíèå èìïëèêàöèé.¬ ∃x1 ( (P(x1 ) & (∀x2 P(x2 )→∃y1 R(x1 , y1 ))) → ∃y2 R(x1 , y2 ) )ÏÐÅÄÂÀÐÅÍÍÛÅ ÍÎÐÌÀËÜÍÛÅ ÔÎÐÌÛÄîêàçàòåëüñòâî2. Óäàëåíèå èìïëèêàöèé.¬ ∃x1 ( (P(x1 ) & (∀x2 P(x2 )→∃y1 R(x1 , y1 ))) → ∃y2 R(x1 , y2 ) )¬ ∃x1 ( ¬(P(x1 ) & (¬∀x2 P(x2 )∨∃y1 R(x1 , y1 ))) ∨ ∃y2 R(x1 , y2 ) )ÏÐÅÄÂÀÐÅÍÍÛÅ ÍÎÐÌÀËÜÍÛÅ ÔÎÐÌÛÄîêàçàòåëüñòâî3. Ïðîäâèæåíèå îòðèöàíèÿ âãëóáü.Ïðèìåíÿåì ðàâíîñèëüíîñòè|= ¬¬ϕ ≡ ϕ,∨|= ¬(ϕ &∨ ψ) ≡ ¬ϕ & ¬ψ ,|= ¬ ∀∃ xϕ ≡∃∀x¬ϕÏÐÅÄÂÀÐÅÍÍÛÅ ÍÎÐÌÀËÜÍÛÅ ÔÎÐÌÛÄîêàçàòåëüñòâî3. Ïðîäâèæåíèå îòðèöàíèÿ âãëóáü.¬ ∃x1 ( ¬(P(x1 ) & (¬∀x2 P(x2 ) ∨ ∃y1 R(x1 , y1 ))) ∨ ∃y2 R(x1 , y2 ) )ÏÐÅÄÂÀÐÅÍÍÛÅ ÍÎÐÌÀËÜÍÛÅ ÔÎÐÌÛÄîêàçàòåëüñòâî3.
