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

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

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

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

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

. . 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.

Ïðîäâèæåíèå îòðèöàíèÿ âãëóáü.¬ ∃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. Ïðîäâèæåíèå îòðèöàíèÿ âãëóáü.¬ ∃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 ) )∀x1 ( ¬¬(P(x1 ) & (¬∀x2 P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ¬∃y2 R(x1 , y2 ) )ÏÐÅÄÂÀÐÅÍÍÛÅ ÍÎÐÌÀËÜÍÛÅ ÔÎÐÌÛÄîêàçàòåëüñòâî3. Ïðîäâèæåíèå îòðèöàíèÿ âãëóáü.¬ ∃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 ) )∀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.

Ïðîäâèæåíèå îòðèöàíèÿ âãëóáü.¬ ∃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 ) )∀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 ) )∀x1 ( (P(x1 ) & (∃x2 ¬P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ∀y2 ¬R(x1 , y2 ) )ÏÐÅÄÂÀÐÅÍÍÛÅ ÍÎÐÌÀËÜÍÛÅ ÔÎÐÌÛÄîêàçàòåëüñòâî4. Âûíåñåíèå êâàíòîðîâ ¾íàðóæó¿.Ïðèìåíÿåìðàâíîñèëüíîñòè|= ∀∃ xϕ(x)&ψ ≡ ∀∃ x(ϕ(x)&ψ),|= ∀∃ xϕ(x) ∨ ψ ≡ ∀∃ x(ϕ(x) ∨ ψ),&|= ϕ &∨ ψ ≡ ψ ∨ ϕ.ÏÐÅÄÂÀÐÅÍÍÛÅ ÍÎÐÌÀËÜÍÛÅ ÔÎÐÌÛÄîêàçàòåëüñòâî4. Âûíåñåíèå êâàíòîðîâ ¾íàðóæó¿.∀x1 ( (P(x1 ) & (∃x2 ¬P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ∀y2 ¬R(x1 , y2 ) )ÏÐÅÄÂÀÐÅÍÍÛÅ ÍÎÐÌÀËÜÍÛÅ ÔÎÐÌÛÄîêàçàòåëüñòâî4.

Âûíåñåíèå êâàíòîðîâ ¾íàðóæó¿.∀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 ) )ÏÐÅÄÂÀÐÅÍÍÛÅ ÍÎÐÌÀËÜÍÛÅ ÔÎÐÌÛÄîêàçàòåëüñòâî4. Âûíåñåíèå êâàíòîðîâ ¾íàðóæó¿.∀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 ) )∀x1 ( ∃x2 (P(x1 ) & (¬P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ∀y2 ¬R(x1 , y2 ) )ÏÐÅÄÂÀÐÅÍÍÛÅ ÍÎÐÌÀËÜÍÛÅ ÔÎÐÌÛÄîêàçàòåëüñòâî4. Âûíåñåíèå êâàíòîðîâ ¾íàðóæó¿.∀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 ) )∀x1 ( ∃x2 (P(x1 ) & (¬P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ∀y2 ¬R(x1 , y2 ) )∀x1 ∃x2 ( (P(x1 ) & (¬P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ∀y2 ¬R(x1 , y2 ) )è òàê äàëåå...ÏÐÅÄÂÀÐÅÍÍÛÅ ÍÎÐÌÀËÜÍÛÅ ÔÎÐÌÛÄîêàçàòåëüñòâî4. Âûíåñåíèå êâàíòîðîâ ¾íàðóæó¿.∀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 ) )∀x1 ( ∃x2 (P(x1 ) & (¬P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ∀y2 ¬R(x1 , y2 ) )∀x1 ∃x2 ( (P(x1 ) & (¬P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ∀y2 ¬R(x1 , y2 ) )è òàê äàëåå...∀x1 ∃x2 ∃y1 ∀y2 ( (P(x1 ) & (¬P(x2 ) ∨ R(x1 , y1 ))) & ¬R(x1 , y2 ) )ÏÐÅÄÂÀÐÅÍÍÛÅ ÍÎÐÌÀËÜÍÛÅ ÔÎÐÌÛÄîêàçàòåëüñòâî5.

Ïðèâåäåíèå ìàòðèöû ê êîíúþíêòèâíîé íîðìàëüíîé ôîðìå.Ïðèìåíÿåì çàêîíû áóëåâîé àëãåáðû.ÏÐÅÄÂÀÐÅÍÍÛÅ ÍÎÐÌÀËÜÍÛÅ ÔÎÐÌÛÄîêàçàòåëüñòâî5. Ïðèâåäåíèå ìàòðèöû ê êîíúþíêòèâíîé íîðìàëüíîé ôîðìå.ψ = ∀x1 ∃x2 ∃y1 ∀y2 (P(x1 ) & (¬P(x2 ) ∨ R(x1 , y1 )) & ¬R(x1 , y2 ) ) ðåçóëüòàòå ïîëó÷àåì ôîðìóëó ψ, êîòîðàÿI ÿâëÿåòñÿ ïðåäâàðåííîé íîðìàëüíîé ôîðìîé,I ðàâíîñèëüíà èñõîäíîé ôîðìóëå ϕ.ÎÁÙÀß ÑÕÅÌÀ ÌÅÒÎÄÀ ÐÅÇÎËÞÖÈÉÈñõîäíàÿôîðìóëà-ϕÑÑÔϕ2Ñèñòåìàäèçúþíêòîâ¬ϕ?ÏÍÔϕ1?SϕÎòðèöàíèå-Ðåçîëþòèâíûé âûâîäïóñòîãî äèçúþíêòà èç ñèñòåìû SϕÑÊÎËÅÌÎÂÑÊÈÅ ÑÒÀÍÄÀÐÒÍÛÅ ÔÎÐÌÛÎïðåäåëåíèåÏðåäâàðåííàÿ íîðìàëüíàÿ ôîðìà âèäàϕ = ∀xi1 ∀xi2 .

. . ∀xim M(xi1 , xi2 , . . . , xim ),â êîòîðîé êâàíòîðíàÿ ïðèñòàâêà íå ñîäåðæèò êâàíòîðîâ ∃,íàçûâàåòñÿ ñêîëåìîâñêîé ñòàíäàðòíîé ôîðìîé (ÑÑÔ) .Ïðèìåðû ÑÑÔ∀x1 ∀y2 (P(x1 ) & (¬P(f (x1 )) ∨ R(x1 , g (x1 ))) & ¬R(x1 , y2 ) )R(c1 , f (c1 , c2 )) ∨ P(c2 )ÑÊÎËÅÌÎÂÑÊÈÅ ÑÒÀÍÄÀÐÒÍÛÅ ÔÎÐÌÛÒåîðåìà î ÑÑÔÄëÿ ëþáîé çàìêíóòîé ôîðìóëû ϕ ñóùåñòâóåò òàêàÿñêîëåìîâñêàÿ ñòàíäàðòíàÿ ôîðìà ψ, ÷òîϕ âûïîëíèìàÄîêàçàòåëüñòâî⇐⇒ψ âûïîëíèìà.Âîñïîëüçóåìñÿ ëåììîé îá óäàëåíèè êâàíòîðîâ ñóùåñòâîâàíèÿ .ÑÊÎËÅÌÎÂÑÊÈÅ ÑÒÀÍÄÀÐÒÍÛÅ ÔÎÐÌÛËåììà îá óäàëåíèè êâàíòîðîâ ñóùåñòâîâàíèÿÏóñòü ϕ = ∀x1∀x2 . .

. ∀xk ∃xk+1 ϕ0(x1, x2, . . . , xk , xk+1) çàìêíóòàÿ(k)ôîðìóëà, k ≥ 0, è k -ìåñòíûé ôóíêöèîíàëüíûéñèìâîë f íå ñîäåðæèòñÿ â ôîðìóëå ϕ.Òîãäà ôîðìóëà ϕ âûïîëíèìà â òîì è òîëüêî òîì ñëó÷àå,êîãäà âûïîëíèìà ôîðìóëà(k)ψ = ∀x1 ∀x2 . . . ∀xk ϕ0 (x1 , x2 , . . . , xk , fÄîêàçàòåëüñòâî ëåììû.(x1 , x2 , . . . , xk )).(⇐ ) Ïóñòü I ìîäåëü äëÿ ψ.Òîãäà äëÿ ëþáîãî íàáîðà d1, d2, . . .

, dk ∈ DI èìååò ìåñòîI |= ϕ0 [d1 , d2 , . . . , dk , f (k) (d1 , d2 , . . . , dk )],ò. å. äëÿ ëþáîãî íàáîðà d1, d2, . . . , dk ∈ DI ñóùåñòâóåò òàêîéýëåìåíò dk+1 = f (k)(d1, d2, . . . , dk ), ÷òîI |= ϕ0 [d1 , d2 , . . . , dk , dk+1 ].Ýòî îçíà÷àåò, ÷òî I |= ∀x1∀x2 . . . ∀xk ∃xk+1ϕ0.ÑÊÎËÅÌÎÂÑÊÈÅ ÑÒÀÍÄÀÐÒÍÛÅ ÔÎÐÌÛÄîêàçàòåëüñòâî ëåììû îá óäàëåíèè∃.(⇒ ) Ïóñòü I ìîäåëü äëÿ ϕ. Òîãäà äëÿ ëþáîãî íàáîðàd1 , d2 , .

. . , dk ∈ DI ñóùåñòâóåò òàêîé ýëåìåíò dk+1 ∈ DI , ÷òîI |= ϕ0 [d1 , d2 , . . . , dk , dk+1 ].Ïóñòü f : DIk → DI ýòî íåêîòîðàÿ ôóíêöèÿ, âû÷èñëÿþùàÿäëÿ êàæäîãî íàáîðà d1, d2, . . . , dk ∈ DI òàêîé ýëåìåíòdk+1 = f(d1 , d2 , . . . , dk ), ÷òîI |= ϕ0 [d1 , d2 , .

. . , dk , dk+1 ].Ðàññìîòðèì èíòåðïðåòàöèþ I 0, êîòîðàÿ îòëè÷àåòñÿ îò I òîëüêîòåì, ÷òî îöåíêîé ôóíêöèîíàëüíîãî ñèìâîëà f (k) ÿâëÿåòñÿôóíêöèÿ f .Òîãäà äëÿ ëþáîãî íàáîðà d1, d2, . . . , dk âåðíîI 0 |= ϕ0 [d1 , d2 , . . . , dk , f (k) (d1 , d2 , . . . , dk )]. (ïî÷åìó? )Ýòî îçíà÷àåò, ÷òîI 0 |= ∀x1 ∀x2 . . . ∀xk ϕ0 (x1 , x2 , . .

. , xk , f (k) (x1 , x2 , . . . , xk )).ÑÊÎËÅÌÎÂÑÊÈÅ ÑÒÀÍÄÀÐÒÍÛÅ ÔÎÐÌÛÏðîäîëæåíèå äîêàçàòåëüñòâà òåîðåìû îá ÑÑÔÓäàëÿåì ïî î÷åðåäè êâàíòîðû ñóùåñòâîâàíèÿ ñ ïîìîùüþëåììû.ϕ = ∀x1 . . . ∀xk ∃xk+1 ∀xk+2 . . . ∀xm ∃xm+1 . . .ϕ0 (x1 , . . . , xk , xk+1 , xk+2 . . . xm , xm+1 , . . . )ϕ0 = ∀x1 . . . ∀xk ∀xk+2 . .

. ∀xm ∃xm+1 . . .ϕ0 (x1 , . . . , xk , f (x1 , . . . , xk ), xk+2 . . . xm , xm+1 , . . . )ϕ00 = ∀x1 . . . ∀xk ∀xk+2 . . . ∀xm . . .ϕ0 (x1 , . . . , xk , f (x1 , . . . , xk ), xk+2 . . . xm , g (x1 , . . . , xk , xk+2 , . . . , xm ), . . . )è. ò. ä.Ïðè ýòîì âûïîëíèìîñòü ôîðìóë ñîõðàíÿåòñÿ.ÑÊÎËÅÌÎÂÑÊÈÅ ÑÒÀÍÄÀÐÒÍÛÅ ÔÎÐÌÛÏðèìåðϕ = ∀x1 ∃x2 ∃y1 ∀y2 (P(x1 ) & (¬P(x2 ) ∨ R(x1 , y1 )) & ¬R(x1 , y2 ) )ÑÊÎËÅÌÎÂÑÊÈÅ ÑÒÀÍÄÀÐÒÍÛÅ ÔÎÐÌÛÏðèìåðϕ = ∀x1 ∃x2 ∃y1 ∀y2 (P(x1 ) & (¬P(x2 ) ∨ R(x1 , y1 )) & ¬R(x1 , y2 ) )ϕ0 = ∀x1 ∃y1 ∀y2 (P(x1 ) & (¬P(f (x1 )) ∨ R(x1 , y1 )) & ¬R(x1 , y2 ) )ÑÊÎËÅÌÎÂÑÊÈÅ ÑÒÀÍÄÀÐÒÍÛÅ ÔÎÐÌÛÏðèìåðϕ = ∀x1 ∃x2 ∃y1 ∀y2 (P(x1 ) & (¬P(x2 ) ∨ R(x1 , y1 )) & ¬R(x1 , y2 ) )ϕ0 = ∀x1 ∃y1 ∀y2 (P(x1 ) & (¬P(f (x1 )) ∨ R(x1 , y1 )) & ¬R(x1 , y2 ) )ϕ00 = ∀x1 ∀y2 (P(x1 ) & (¬P(f (x1 )) ∨ R(x1 , g (x1 ))) & ¬R(x1 , y2 ) )ϕâûïîëíèìà⇐⇒ϕ00âûïîëíèìà.ÑÊÎËÅÌÎÂÑÊÈÅ ÑÒÀÍÄÀÐÒÍÛÅ ÔÎÐÌÛÒåðì f (k)(x1, .

Свежие статьи
Популярно сейчас