Лекция 6. Общая схема метода резолюций. Равносильные формулы. Теорема о равносильной замене... (1161877)
Текст из файла
Îñíîâûìàòåìàòè÷åñêîéëîãèêèèëîãè÷åñêîãîïðîãðàììèðîâàíèÿËÅÊÒÎÐ: Â.À. Çàõàðîâ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.
Характеристики
Тип файла PDF
PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.
Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
