Лекция 6. Общая схема метода резолюций. Равносильные формулы. Теорема о равносильной замене... (Лекции 2014), страница 2
Описание файла
Файл "Лекция 6. Общая схема метода резолюций. Равносильные формулы. Теорема о равносильной замене..." внутри архива находится в папке "Лекции 2014". PDF-файл из архива "Лекции 2014", который расположен в категории "". Всё это находится в предмете "математическая логика и логическое программирование" из 8 семестр, которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст 2 страницы из PDF
Ïðîäâèæåíèå îòðèöàíèÿ âãëóáü.¬ ∃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, .
. . , xk ), êîòîðûé ïîäñòàâëÿåòñÿ âìåñòî óäàëÿåìîéïåðåìåííîé xk+1, ñâÿçàííîé êâàíòîðîì ∃, íàçûâàåòñÿñêîëåìîâñêèì òåðìîì .Åñëè k = 0, òî òåðì íàçûâàåòñÿ ñêîëåìîâñêîé êîíñòàíòîé .Ïðîöåäóðà óäàëåíèÿ êâàíòîðîâ ∃ íàçûâàåòñÿ ñêîëåìèçàöèåé .ÎÁÙÀß ÑÕÅÌÀ ÌÅÒÎÄÀ ÐÅÇÎËÞÖÈÉÈñõîäíàÿôîðìóëà-ϕÑÑÔϕ2Ñèñòåìàäèçúþíêòîâ¬ϕ?ÏÍÔϕ1?SϕÎòðèöàíèå-Ðåçîëþòèâíûé âûâîäïóñòîãî äèçúþíêòà èç ñèñòåìû SϕÑÈÑÒÅÌÛ ÄÈÇÚÞÍÊÒÎÂÓòâåðæäåíèå|= ∀x(ϕ&ψ) ≡ ∀xϕ&∀xψÈíà÷å ãîâîðÿ, êâàíòîðû ∀ ìîæíî ðàâíîìåðíî ðàñïðåäåëèòü ïîñîìíîæèòåëÿì (äèçúþíêòàì) ÊÍÔ.ÒåîðåìàÑêîëåìîâñêàÿ ñòàíäàðòíàÿ ôîðìàϕ = ∀x1 ∀x2 .
. . ∀xm (D1 & D2 & . . . & DN )íåâûïîëíèìà òîãäà è òîëüêî òîãäà, êîãäà ìíîæåñòâî ôîðìóëSϕ = {∀x1 ∀x2 . . . ∀xm D1 , ∀x1 ∀x2 . . . ∀xm D2 , . . . , ∀x1 ∀x2 . . . ∀xm DN }íå èìååò ìîäåëè.ÑÈÑÒÅÌÛ ÄÈÇÚÞÍÊÒÎÂÊàæäàÿ ôîðìóëà ìíîæåñòâà Sϕ èìååò âèä∀x1 ∀x2 . . . ∀xm (L1 ∨ L2 ∨ · · · ∨ Lk )è íàçûâàåòñÿ äèçúþíêòîì . äàëüíåéøåì (ïî óìîë÷àíèþ) áóäåì ïîëàãàòü, ÷òî âñåïåðåìåííûå äèçúþíêòà ñâÿçàíû êâàíòîðàìè ∀, è êâàíòîðíóþïðèñòàâêó âûïèñûâàòü íå áóäåì.Êàæäûé äèçúþíêò ñîñòîèò èç ëèòåð L1, L2, . . .
, Lk .Ëèòåðà ýòî ëèáî àòîì, ëèáî îòðèöàíèå àòîìà.Îñîáî âûäåëåí äèçúþíêò, â êîòîðîì íåò íè îäíîé ëèòåðû.Òàêîé äèçúþíêò íàçûâàåòñÿ ïóñòûì äèçúþíêòîì èîáîçíà÷àåòñÿ . Ïóñòîé äèçúþíêò òîæäåñòâåííî ëîæåí(ïî÷åìó? ).Ïîòîìó ÷òî |= L1 ∨ · · · ∨ Lk ≡ L1 ∨ · · · ∨ Lk ∨ false, è ïîýòîìóïðè k = 0 èìååì |= ≡ false.ÑÈÑÒÅÌÛ ÄÈÇÚÞÍÊÒÎÂÑèñòåìó äèçúþíêòîâ, íå èìåþùóþ ìîäåëåé, áóäåì íàçûâàòüíåâûïîëíèìîé , èëè ïðîòèâîðå÷èâîé ñèñòåìîé äèçúþíêòîâ.Çàäà÷à ïðîâåðêè îáùåçíà÷èìîñòè ôîðìóë ëîãèêè ïðåäèêàòîâ.|= ϕ ?îáùåçíà÷èìà ⇐⇒ ϕ0 = ¬ϕ íåâûïîëíèìà.ϕ0 íåâûïîëíèìà ⇐⇒ ÏÍÔ ϕ1 íåâûïîëíèìà.ϕ1 íåâûïîëíèìà ⇐⇒ ÑÑÔ ϕ2 íåâûïîëíèìà.ϕ2 íåâûïîëíèìà ⇐⇒ ñèñòåìà äèçúþíêòîâ Sϕ íåâûïîëíèìà.Èòàê, ïðîâåðêà îáùåçíà÷èìîñòè |= ϕ ? ñâîäèòñÿ ê ïðîâåðêåïðîòèâîðå÷èâîñòè ñèñòåìû äèçúþíêòîâ Sϕ.ϕÑÈÑÒÅÌÛ ÄÈÇÚÞÍÊÒÎÂ: ÏÐÈÌÅÐÈñõîäíàÿ ôîðìóëà:ϕ = ∃x( (P(x) & (∀xP(x) → ∃yR(x, y ))) → ∃yR(x, y ) )Åå îòðèöàíèå:ϕ0 = ¬ ∃x( (P(x) & (∀xP(x) → ∃yR(x, y ))) → ∃yR(x, y ) )Ïðåäâàðåííàÿ íîðìàëüíàÿ ôîðìà äëÿ ϕ0:ϕ1 = ∀x1 ∃x2 ∃y1 ∀y2 (P(x1 ) & (¬P(x2 ) ∨ R(x1 , y1 )) & ¬R(x1 , y2 ) )Ñêîëåìîâñêàÿ ñòàíäàðòíàÿ ôîðìà:ϕ2 = ∀x1 ∀y2 (P(x1 ) & (¬P(f (x1 )) ∨ R(x1 , g (x1 ))) & ¬R(x1 , y2 ) )ÑÈÑÒÅÌÛ ÄÈÇÚÞÍÊÒÎÂ: ÏÐÈÌÅÐÑèñòåìà äèçúþíêòîâ:Sϕ = {D1 = P(x1 ),D2 = ¬P(f (x1 )) ∨ R(x1 , g (x1 )),D3 = ¬R(x1 , y2 )}Çàäà÷à:êàê ïðîâåðèòü ïðîòèâîðå÷èâîñòüïðîèçâîëüíîé ñèñòåìûäèçúþíêòîâ?ÊÎÍÅÖ ËÅÊÖÈÈ 6..