Расширенный сборник задач для самостоятельного решения (1161810), страница 5
Текст из файла (страница 5)
Êàêèåèç ïðèâåäåííûõ íèæå óòâåðæäåíèé âñåãäà ñïðàâåäëèâû è ïî÷åìó?1. Åñëè êàæäûé äèçúþíêò ìíîæåñòâà S0 âûïîëíèì, òî è êàæäûé äèçúþíêò ìíîæåñòâà S1âûïîëíèì, ïîòîìó ÷òî....2. Åñëè êàæäûé äèçúþíêò ìíîæåñòâà S1 âûïîëíèì, òî ìíîæåñòâî äèçúþíêòîâ S0 èìååòìîäåëü, ïîòîìó ÷òî....3.
Åñëè ìíîæåñòâî äèçúþíêòîâ S0 èìååò ìîäåëü, òî ìíîæåñòâî äèçúþíêòîâ S1 èìååò ìîäåëü, ïîòîìó ÷òî....Óïðàæíåíèå 1.87.Îñòàíåòñÿ ëè âåðíîé òåîðåìà ïîëíîòû ðåçîëþòèâíîãî âûâîäà â òîìñëó÷àå, åñëè ïðè ïîñòðîåíèè âûâîäà íå ïîëüçîâàòüñÿ ïðàâèëîì ñêëåéêè?Óïðàæíåíèå 1.88.Ïðåäïîëîæèì, ÷òî â ïðàâèëî ðåçîëþöèè áûëî âíåñåíî ñëåäóþùåå èçìåíåíèå: ðåçîëüâåíòîé äèçúþíêòîâ D1 = D10 ∨L1 è D2 = D20 ∨¬L2 îáúÿâëÿåòñÿ âñÿêèé äèçúþíêòD0 = (D10 ∨ D20 )η , ãäå η íåêîòîðûé óíèôèêàòîð (íåîáÿçàòåëüíî íàèáîëåå îáùèé) ëèòåð L1è L2 .
Êàêèå èç ïðèâåäåííûõ íèæå óòâåðæäåíèé áóäóò ñïðàâåäëèâû è ïî÷åìó?1. Ïîñëå òàêîãî èçìåíåíèÿ è òåîðåìà êîððåêòíîñòè ðåçîëþòèâíîãî âûâîäà è òåîðåìà ïîëíîòû ðåçîëþòèâíîãî âûâîäà óæå áóäóò íåâåðíû, ïîòîìó ÷òî...2. Ïîñëå òàêîãî èçìåíåíèÿ òåîðåìà êîððåêòíîñòè ðåçîëþòèâíîãî âûâîäà îñòàåòñÿ âåðíîé,à òåîðåìà ïîëíîòû ðåçîëþòèâíîãî âûâîäà óæå áóäåò íåâåðíà, ïîòîìó ÷òî...3. Ïîñëå òàêîãî èçìåíåíèÿ òåîðåìà ïîëíîòû ðåçîëþòèâíîãî âûâîäà îñòàåòñÿ âåðíîé, àòåîðåìà êîððåêòíîñòè ðåçîëþòèâíîãî âûâîäà óæå áóäåò íåâåðíà, ïîòîìó ÷òî...4.
Ïîñëå òàêîãî èçìåíåíèÿ è òåîðåìà êîððåêòíîñòè ðåçîëþòèâíîãî âûâîäà è òåîðåìà ïîëíîòû ðåçîëþòèâíîãî âûâîäà îñòàþòñÿ âåðíûìè, ïîòîìó ÷òî...Óïðàæíåíèå 1.89.1.9.Ïîëíîòà ìåòîäà ðåçîëþöèé23Èçâåñòíî, ÷òî èç ìíîæåñòâà íåïóñòûõ äèçúþíêòîâ S = {D1 , D2 , . . . , DN }ìîæíî ïîñòðîèòü ðåçîëþòèâíûé âûâîä ïóñòîãî äèçúþíêòà . Êàêèå èç ïðèâåäåííûõ íèæåóòâåðæäåíèé âñåãäà ñïðàâåäëèâû è ïî÷åìó?1. Ñóùåñòâóåò óñïåøíûé òàáëè÷íûé âûâîä äëÿ èñõîäíîé òàáëèöû T = h∅, {D1 &D2 & . . . &DN }i,ïîòîìó ÷òî. .
. .2. Ñóùåñòâóåò óñïåøíûé òàáëè÷íûé âûâîä äëÿ èñõîäíîé òàáëèöû T = h{D1 &D2 & . . . &DN }, ∅i,ïîòîìó ÷òî. . . .3. Ñóùåñòâóåò óñïåøíûé òàáëè÷íûé âûâîä äëÿ èñõîäíîé òàáëèöû T = h∅, {D1 ∨ D2 ∨ · · · ∨DN }i, ïîòîìó ÷òî. . . .4. Ñóùåñòâóåò óñïåøíûé òàáëè÷íûé âûâîä äëÿ èñõîäíîé òàáëèöû T = h{D1 ∨ D2 ∨ · · · ∨DN }, ∅i, ïîòîìó ÷òî.
. . .Óïðàæíåíèå 1.90.Ïóñòü S - ýòî íåêîòîðîå ìíîæåñòâî äèçúþíêòîâ, à [S] - ýòî ìíîæåñòâîâñåõ îñíîâíûõ ïðèìåðîâ äèçúþíêòîâ èç ìíîæåñòâà S. Êàêèå èç ïðèâåäåííûõ íèæå óòâåðæäåíèé âñåãäà ñïðàâåäëèâû è ïî÷åìó?1. Åñëè äèçúþíêò D ðåçîëþòèâíî âûâîäèì èç ìíîæåñòâà äèçúþíêòîâ S , òî ýòîò æå äèçúþíêò D ðåçîëþòèâíî âûâîäèì èç ìíîæåñòâà îñíîâíûõ ïðèìåðîâ äèçúþíêòîâ [S], ïîòîìó÷òî...2. Åñëè äèçúþíêò D ðåçîëþòèâíî âûâîäèì èç ìíîæåñòâà îñíîâíûõ ïðèìåðîâ äèçúþíêòîâ[S], òî ýòîò æå äèçúþíêò D ðåçîëþòèâíî âûâîäèì èç ìíîæåñòâà äèçúþíêòîâ S , ïîòîìó÷òî...3. Åñëè ýðáðàíîâñêàÿ èíòåðïðåòàöèÿ I ÿâëÿåòñÿ ìîäåëüþ äëÿ ìíîæåñòâà äèçúþíêòîâ S ,òî ýòà æå ýðáðàíîâñêàÿ èíòåðïðåòàöèÿ I ÿâëÿåòñÿ ìîäåëüþ äëÿ ìíîæåñòâà îñíîâíûõïðèìåðîâ äèçúþíêòîâ [S], ïîòîìó ÷òî...4. Åñëè ýðáðàíîâñêàÿ èíòåðïðåòàöèÿ I ÿâëÿåòñÿ ìîäåëüþ äëÿ ìíîæåñòâà îñíîâíûõ ïðèìåðîâ äèçúþíêòîâ [S], òî ýòà æå ýðáðàíîâñêàÿ èíòåðïðåòàöèÿ I ÿâëÿåòñÿ ìîäåëüþ äëÿìíîæåñòâà äèçúþíêòîâ S , ïîòîìó ÷òî...Óïðàæíåíèå 1.91.Ïðåäïîëîæèì, ÷òî èç ñèñòåìû äèçúþíêòîâ S ìîæíî ðåçîëþòèâíî âûâåñòè äèçúþíêò P ∨ ¬P .
Êàêèå èç ïðèâåäåííûõ íèæå óòâåðæäåíèé áóäóò âñåãäà âåðíû èïî÷åìó?1.  ñèñòåìå äèçúþíêòîâ S åñòü ïðîòèâîðå÷èâûé äèçúþíêò, ïîòîìó ÷òî. . .2. Ñèñòåìà äèçúþíêòîâ S íåïðîòèâîðå÷èâà, ïîòîìó ÷òî. . .3. Ñèñòåìà äèçúþíêòîâ S ïðîòèâîðå÷èâà, ïîòîìó ÷òî.
. .4. Òàêîé ðåçîëüâåíòû âûâåñòè èç ñèñòåìû äèçúþíêòîâ S íåâîçìîæíî, ïîòîìó ÷òî. . .Óïðàæíåíèå 1.92.24Ãëàâà 1.1.10ÓÏÐÀÆÍÅÍÈßÕîðíîâñêèå ëîãè÷åñêèå ïðîãðàììû. Äåêëàðàòèâíàÿè îïåðàöèîííàÿ ñåìàíòèêè.Óïðàæíåíèå 1.93.Ñëåäóþùèå îñíîâíûå ñâîéñòâà è îòíîøåíèÿìóæ÷èíà(X),• æåíùèíà(Y ),• ìàòü(X, Y ),• îòåö(X, Y ),• ñóïðóãè(X, Y )îïèñûâàþòñÿ ôàêòàìè õîðíîâñêîé ëîãè÷åñêîé ïðîãðàììû, íàïðèìåð,ìóæ÷èíà(adam)←;æåíùèíà(eve)←;îòåö(adam,abel)←;ìàòü(eve,cain)←;Ïðîäîëæèòå ýòó ëîãè÷åñêóþ ïðîãðàììó, ñîçäàâ ïîäõîäÿùèå ïðîãðàììíûå óòâåðæäåíèÿ, îïèñûâàþùèå ñëåäóþùèå ðîäñòâåííûå ñâîéñòâà è îòíîøåíèÿ:1. ðîäèòåëü(X, Y );2.
äåä(X, Y );3. áûòü_îòöîì(X);4. áðàò(X, Y );5. ñâîÿ÷åíèöà(X, Y );6. ïðåäîê(X, Y );7. ïîòîìîê(X, Y );8. ðîäñòâåííèê(X, Y );•Óïðàæíåíèå 1.94.òåðìîâ:Ñîçäàéòå ëîãè÷åñêèå ïðîãðàììû, îïèñûâàþùèå ñëåäóþùèå ñâîéñòâà "Y ÿâëÿåòñÿ ñïèñêîì".elem(X, Y ) "X ÿâëÿåòñÿ ýëåìåíòîì ñïèñêà YÂûÿñíèòü, êàêîâî ìíîæåñòâî ïðàâèëüíûõ îòâåòîâ íà ñëåäóþùèå çàïðîñû, îáðàùåííûå ê ïîñòðîåííûì ïðîãðàììàì:1.
? list(a.b.c.nil)list(X)1.10.2.3.4.5.6.7.Õîðíîâñêèå ëîãè÷åñêèå ïðîãðàììû. Äåêëàðàòèâíàÿ è îïåðàöèîííàÿ ñåìàíòèêè.25? list(a.X.nil)? list(a.b)? list(a.Y)? elem(b,a.b.c.nil)? elem(X,a.b.c.nil)? elem(a,X)Ïîñòðîéòå SLD-ðåçîëþòèâíûå âû÷èñëåíèÿ äëÿ êàæäîãî èç çàïðîñîâ,ïðèâåäåííûõ â óïðàæíåíèè 1.94, îáðàùåííûõ ê ïðîãðàììàì, îïèñûâþùèì ïðåäèêàòû list èelem.Ïîñòðîéòå âñåâîçìîæíûå SLD-ðåçîëþòèâíûå âû÷èñëåíèÿ äëÿ çàïðîñàG= ? R(Y),P(Z), îáðàùåííîãî ê ïðîãðàììå P , âûäåëÿÿ â êàæäîì öåëåâîì óòâåðæäåíèè ñàìóþëåâóþ ïîäöåëü. Êàêîâî ìíîæåñòâî âû÷èñëåííûõ îòâåòîâ íà çàïðîñ G ê ïðîãðàììå P ?P : R(Y) ← P(Y),Q(Y);Óïðàæíåíèå 1.95.Óïðàæíåíèå 1.96.P(a) ← ;P(b) ← ;Q(a) ← ;Q(f(X)) ← Q(X);Ïîñòðîèòü ëîãè÷åñêèå ïðîãðàììû, îïèñûâàþùèå ñëåäóþùèå ñâîéñòâàè îòíîøåíèÿ íà ìíîæåñòâå ñïèñêîâ.Óïðàæíåíèå 1.97.1.2.3.4.5.6.7.8.9.10.: Çàãîëîâêîì ñïèñêà L ÿâëÿåòñÿ ýëåìåíò X ;tail(L, X) : Õâîñòîì ñïèñêà L ÿâëÿåòñÿ ñïèñîê X ;pref ix(L, X) : Ïðåôèêñîì (íà÷àëüíûì ïîäñïèñêîì) ñïèñêà L ÿâëÿåòñÿ ñïèñîê X ;suf f ix(L, X) : Ñóôôèêñîì (çàêëþ÷èòåëüíûì ïîäñïèñêîì) ñïèñêà L ÿâëÿåòñÿ ñïèñîê X ;sublist(L, X) : Ñïèñîê X ÿâëÿåòñÿ ïîäñïèñêîì ñïèñêà L;equal(X, Y ) : Ñïèñêè X è Y ñîâïàäàþò;equal_length(X, Y ) : Ñïèñêè X è Y èìåþò îäèíàêîâóþ äëèíó;nonequal_length(X, Y ) : Ñïèñêè X è Y ðàçíóþ äëèíó;less(X, Y ) : Äëèíà ñïèñêà X ìåíüøå äëèíû ñïèñêà Y ;subset(X, Y ) : Ñïèñîê X ñîñòîèò òîëüêî èç ýëåìåíòîâ, ñîäåðæàùèõñÿ â ñïèñêå Y ;head(L, X)2611.12.13.14.15.16.17.18.19.20.21.22.23.24.25.Ãëàâà 1.ÓÏÐÀÆÍÅÍÈß: Ñïèñîê X ÿâëÿåòñÿ êîíêàòåíàöèåé (ïîñëåäîâàòåëüíûì ñîåäèíåíèåì)ñïèñêîâ è ;reverse(X, Y ) : Ñïèñîê X ÿâëÿåòñÿ îáðàùåíèåì ñïèñêà Y , ò.
å. X ñîñòîèò èç òåõ æåýëåìåíòîâ, ÷òî è ñïèñîê Y , íî â ñïèñêå X ýòè ýëåìåíòû ñëåäóþò äðóã çà äðóãîì âîáðàòíîì ïîðÿäêå;palindrome(X, Y ) : Ñïèñîê X ÿâëÿåòñÿ ïàëèíäðîìîì Y , ò. å. X îäèíàêîâî ïðî÷èòûâàåòñÿñëåâà íàïðàâî è ñïðàâî íàëåâî;delete(X, Y ) : Ñïèñîê X îáðàçîâàí èç ñïèñêà Y óäàëåíèåì îäíîãî èëè íåñêîëüêèõ ïîäðÿäèäóùèõ ýëåìåíòîâ;subsequence(X, Y ) : Ïîñëåäîâàòåëüíîñòü X ÿâëÿåòñÿ ïîäïîñëåäîâàòåëüíîñòüþ ïîñëåäîâàòåëüíîñòè Y ;summ(X, Y, Z) : Äëèíà ñïèñêà X ðàâíà ñóììå äëèí ñïèñêîâ Y è Z ;product(X, Y, Z) : Äëèíà ñïèñêà X ðàâíà ïðîèçâåäåíèþ äëèí ñïèñêîâ Y è Z ;dif f er(X, Y, Z) : Äëèíà ñïèñêà X ðàâíà àáñîëþòíîé ðàçíîñòè äëèí ñïèñêîâ Y è Z ;multiple(X, Y ) : Äëèíà ñïèñêà X êðàòíà äëèíå ñïèñêà Y ;nonmultiple(X, Y ) : Äëèíà ñïèñêà X íå êðàòíà äëèíå ñïèñêà Y ;period(X, Y ) : Ñïèñîê X ÿâëÿåòñÿ ïåðèîäè÷åñêîé ïîñëåäîâàòåëüíîñòüþ, ïîëó÷åííîé âðåçóëüòàòå ìíîãîêðàòíîãî ïîâòîðåíèÿ ñïèñêà Y ;stuttering(X) : Ñïèñîê X îáðàçîâàí â ðåçóëüòàòå íåîäíîêðàòíîãî ïîâòîðåíèÿ íåêîòîðîãîäðóãîãî ñïèñêà;power2(X) : Äëèíà ñïèñêà X ÿâëÿåòñÿ ñòåïåíüþ ÷èñëà 2;prime(X) : Äëèíà ñïèñêà X ÿâëÿåòñÿ ïðîñòûì ÷èñëîì;progression(X) : Âñå ýëåìåíòû ñïèñêà X ýòî ñïèñêè, äëèíû êîòîðûõ (â ïîðÿäêå ñëåäîâàíèÿ ýëåìåíòîâ â ñïèñêå X ) îáðàçóþò àðèôìåòè÷åñêóþ ïðîãðåññèþ;concat(X, Y, Z)Y ZÏóñòü σ = hConst, F unc, P redi óñëîâèìñÿ îáîçíà÷àòü Hσ ýðáðàíîâñêèé óíèâåðñóì (ìíîæåñòâî îñíîâíûõ òåðìîâ) ñèãíàòóðû σ, à Bσ ýðáðàíîâñêèé áàçèñ ñèãíàòóðû (ìíîæåñòâîîñíîâíûõ àòîìîâ) σ.
Òîãäà êàæäàÿ ýðáðàíîâñêàÿ èíòåðïðåòàöèÿ I ñèãíàòóðû ïîëíîñòüþ îïðåäåëÿåòñÿ ìíîæåñòâîì âñåõ òåõ îñíîâíûõ àòîìîâ ñèãíàòóðû σ, êîòîðûå âûïîëíÿþòñÿ â èíòåðïðåòàöèè I . Â ïîñëåäóþùèõ óïðàæíåíèÿõ áóäåò èñïîëüçîâàòüñÿ òåîðåòèêî-ìíîæåñòâåííûéñïîñîá ïðåäñòàâëåíèÿ ýðáðàíîâñêèõ èíòåðïðåòàöèé, ïðè êîòîðîì ýðáðàíîâñêàÿ èíòåðïðåòàöèÿ I îòîæäåñòâëÿåòñÿ ñ òåì ìíîæåñòâîì îñíîâíûõ àòîìîâ, êîòîðûå â íåé âûïîëíÿþòñÿ,ò.
å.I = {A : A ∈ Bσ , I |= A}.Òîãäà I íàçûâàåòñÿ ýðáðàíîâñêîé ìîäåëüþ äëÿ õîðíîâñêîé ëîãè÷åñêîé ïðîãðàììû P , åñëè äëÿëþáîãî ïðîãðàììíîãî óòâåðæäåíèÿ D, D ∈ P , ïðåäñòàâëåííîãî â âèäå ëîãè÷åñêîé ôîðìóëû,âåðíîI |= D1.10.Õîðíîâñêèå ëîãè÷åñêèå ïðîãðàììû. Äåêëàðàòèâíàÿ è îïåðàöèîííàÿ ñåìàíòèêè.27Äëÿ îáîçíà÷åíèÿ òîãî ôàêòà, ÷òî ýðáðàíîâñêàÿ èíòåðïðåòàöèÿ I ÿâëÿåòñÿ ìîäåëüþ äëÿ ïðîãðàììû P áóäåò èñïîëüçîâàòüñÿ ñîêðàùåííàÿ çàïèñü I |= P .Äîêàæèòå, ÷òî H -èíòåðïðåòàöèÿ I ÿâëÿåòñÿ ìîäåëüþ äëÿ õîðíîâñêîéëîãè÷åñêîé ïðîãðàììû P òîãäà è òîëüêî òîãäà, êîãäà äëÿ ëþáîãî îñíîâíîãî ïðèìåðà ïðîãðàììíîãî óòâåðæäåíèÿ D0 = A00 ← A01 , . .
. , A0n , D0 ∈ [P] âåðíîÓïðàæíåíèå 1.98.{A01 , . . . , A0n } ⊆ I ⇒ A00 ∈ I.Äîêàæèòå, ÷òî êàæäàÿ õîðíîâñêàÿ ëîãè÷åñêàÿ ïðîãðàììà P èìååò õîòÿáû îäíó ýðáðàíîâñêóþ ìîäåëü.Äîêàæèòå, ÷òî H -èíòåðïðåòàöèÿ BH ÿâëÿåòñÿ ìîäåëüþ äëÿ ëþáîéõîðíîâñêîé ëîãè÷åñêîé ïðîãðàììû P . Ïðèâåäèòå ïðèìåð ïðîãðàììû, ìîäåëüþ êîòîðîé ÿâëÿåòñÿ èíòåðïðåòàöèÿ I = ∅. Êàê äîëæíà áûòü óñòðîåíà ïðîãðàììà P äëÿ òîãî, ÷òîáû èíòåðïðåòàöèÿ I = ∅ áûëà åå ìîäåëüþ?Äîêàæèòå, ÷òî åñëè H -èíòåðïðåòàöèè I1 è I2 ÿâëÿþòñÿ ìîäåëÿìèäëÿ õîðíîâñêîé ëîãè÷åñêîé ïðîãðàììû P , òî H -èíòåðïðåòàöèÿ I0 = I1 ∩ I2 òàêæå ÿâëÿåòñÿìîäåëüþ äëÿ P .Ðàññìîòðèì ìíîæåñòâî IP âñåõ ýðáðàíîâñêèõ ìîäåëåé äëÿ ëîãè÷åñêîé ïðîãðàììû P .
Äîêàæèòå, ÷òî H -èíòåðïðåòàöèÿ MP = T I ÿâëÿåòñÿ íàèìåíüøåé (ïîI∈Iîòíîøåíèþ òåîðåòèêî-ìíîæåñòâåííîãî âêëþ÷åíèÿ) ìîäåëüþ äëÿ ïðîãðàììû P .Ðàññìîòðèì ìíîæåñòâî IP âñåõ ýðáðàíîâñêèõ ìîäåëåé äëÿ îãè÷åñêîéïðîãðàììû P . Äîêàæèòå, ÷òî H -èíòåðïðåòàöèÿ MP = T I ÿâëÿåòñÿ íàèìåíüøåé (ïî îòíîI∈Iøåíèþ òåîðåòèêî-ìíîæåñòâåííîãî âêëþ÷åíèÿ) ìîäåëüþ äëÿ ïðîãðàììû P .Äîêàæèòå, ÷òî MP = ∅ òîãäà è òîëüêî òîãäà, êîãäà õîðíîâñêàÿ ëîãè÷åñêàÿ ïðîãðàììà P íå ñîäåðæèò íè îäíîãî ôàêòà.Äîêàæèòå, ÷òî äëÿ ëþáîãî îñíîâíîãî àòîìà A0 è äëÿ ëþáîé õîðíîâñêîé ëîãè÷åñêîé ïðîãðàììû P ñïðàâåäëèâî ñëåäóþùåå ñîîòíîøåíèå:Óïðàæíåíèå 1.99.Óïðàæíåíèå 1.100.Óïðàæíåíèå 1.101.Óïðàæíåíèå 1.102.PÓïðàæíåíèå 1.103.PÓïðàæíåíèå 1.104.Óïðàæíåíèå 1.105.P |= A0 ⇐⇒ A0 ∈ MP .Ïóñòü t1 , t2 , . .
. , tk ýòî íåêîòîðûé íàáîð îñíîâíûõ òåðìîâ.Äîêàæèòå, ÷òî ïîäñòàíîâêà θ = {Y1 /t1 , . . . , Yk /tk } ÿâëÿåòñÿ ïðàâèëüíûì îòâåòîì íà çàïðîñG =?C1 , C2 , . . . , Cm ê õîðíîâñêîé ëîãè÷åñêîé ïðîãðàììå P òîãäà è òîëüêî òîãäà, êîãäà {C1 θ, . . . , Cm θ} ⊆MP .Äîêàæèòå, ÷òî äëÿ ëþáûõ õîðíîâñêèõ ëîãè÷åñêèõ ïðîãðàìì P1 è P2ñïðàâåäëèâî âêëþ÷åíèåÓïðàæíåíèå 1.106.Óïðàæíåíèå 1.107.MP1 ∪ MP2 ⊆ MP1 ∪P2 .28Ãëàâà 1.ÓÏÐÀÆÍÅÍÈßÏðèâåäèòå ïðèìåð ïðîãðàìì P1 è P2 , äëÿ êîòîðûõ óêàçàííîå âêëþ÷åíèå ÿâëÿåòñÿ ñòðîãèì.Êàêèì èç òðåõ òåîðåòèêî-ìíîæåñòâåííûõ îòíîøåíèé ⊆, =, ⊇ ñâÿçàíû ýðáðàíîâñêèå èíòåðïðåòàöèè MP ∩ MP è MP ∩P ?11.11212Òåîðåìû êîððåêòíîñòè è ïîëíîòû äëÿ õîðíîâñêèõ ëîãè÷åñêèõ ïðîãðàìì.Ñîõðàíÿò ëè ñïðàâåäëèâîñòü òåîðåìû êîððåêòíîñòè è ïîëíîòû äëÿõîðíîâñêèõ ëîãè÷åñêèõ ïðîãðàìì, åñëè â îïðåäåëåíèè ïðàâèëà SLD-ðåçîëþöèè âìåñòî íàèáîëåå îáùåãî óíèôèêàòîðà ðàçðåøèòü èñïîëüçîâàòü ïðîèçâîëüíûé óíèôèêàòîð âûäåëåííîéïîäöåëè çàïðîñà è çàãîëîâêà àêòèâèçèðîâàííîãî ïðîãðàììíîãî óòâåðæäåíèÿ?Îïåðàòîðîì íåïîñðåäñòâåííîãî ñëåäîâàíèÿ TP äëÿ õîðíîâñêîé ëîãè÷åñêîé ïðîãðàììû P íàçûâàåòñÿ îòîáðàæåíèåÓïðàæíåíèå 1.108.Óïðàæíåíèå 1.109.TP : 2BP → 2BP ,ñîïîñòàâëÿþùåå êàæäîé ýðáðàíîâñêîé èíòåðïðåòàöèè I, I ⊆ BP , ýðáðàíîâñêóþ èíòåðïðåòàöèþ I 0 = TP (I), I 0 ⊆ BP , óäîâëåòâîðÿþùóþ ñëåäóþùåìó ñîîòíîøåíèþ:I 0 = {A0 : D = A0 ← A1 , .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
