НАЙ-ОБЩ ЧАСТЕН СЛУЧАЙ НА ХОРНОВА ЦЕЛ, ИМАЩ ПРОСТА РЕЗОЛВЕНТА С ДАДЕНА РЕДИЦА ОТ ХОРНОВИ КЛАУЗИ
От предходния въпрос знаем, че когато една хорнова цел има резолвента с дадена крайна редица от хорнови клаузи, някой частен случай на същата цел има проста резолвента със същата редица от клаузи. Ще покажем, че измежду частните случаи на целта, имащи това свойство, съществува един най-общ.
Забележка 1. Би могло да се предположи, че въпросният най-общ частен случай ще може да се намери чрез следствието към края на предходния въпрос, ако вземем в качеството на s1, s2, ..., sn най-общите унификатори, използвани при някое извършване на канонична резолюция на целта с дадената редица от клаузи. Следващият пример показва, че това не винаги е така, ако не се положат някои допълнителни грижи при извършването на каноничната резолюция.
Пример 1. Нека p и r са едноместни предикатни символи, q е едноместен предикатен символ и a е константа. Нека G е целта
?- p(X), q.
Да разгледаме редицата, на която членовете са следните три клаузи:
p(U).
q :– r(X).
r(a).
Вижда се, че празната цел е канонична резолвента на G с горната редица от клаузи, като извършването на каноничната резолюция може да стане с използване на самите три клаузи (а не на други техни варианти) и на най-общи унификатори [U/X], i, [X/a].
По споменатото следствие от предходния въпрос тези субституции водят до следния частен случай на G:
?- p(a), q.
Той обаче не е най-общ измежду частните случаи на G, имащи проста резолвента с разглежданата редица от клаузи, защото самата цел G също има проста резолвента с тази редица. Това би могло да се види чрез канонична резолюция, подобна на гореспоменатата, но с използване на вариант на втората клауза, който е с променлива, различна от X (може да се види и директно, като при простата резолюция с втората клауза си послужим с нейния частен случай, получен чрез субституцията [X/a]).
Нека са дадени една хорнова цел G и една n-членна редица C1, C2, ..., Cn от хорнови клаузи. Ще наричаме добре проведен резолвентен процес за G и C1, C2, ..., Cn такава тройка, състояща се от n+1-членна редица G0, G1, G2, ..., Gn от хорнови цели, n-членна редица C1ў, C2ў, ..., Cnў от хорнови клаузи и n-членна редица s1, s2, ..., sn от субституции, че да имаме равенството G0=G и при i=1,2,...,n да бъдат изпълнени следните условия: целта Gi-1 не е празна, Ciў е вариант на Ci, нямащ общи променливи нито с Gi-1, нито с Gs1s2...si-1, субституцията si е най-общ унификатор на първия член на Gi-1 и главата на Ciў, целта Gi е непосредствената резолвента на Gi-1si и Ciўsi.
Пример 2. Нека целта G е същата както в пример 1, числото n е 3 и редицата C1, C2, ..., Cn е тричленната редица от клаузи в споменатия пример. Един добре проведен резолвентен процес за G и въпросната редица е например онзи, при който в качеството на G0, G1, G2, G3, C1ў, C2ў, C3ў, s1, s2, s3 са взети съответно целта G, целта с единствен член q, целта с единствен член r(Y), празната цел, клаузите C1, C2[X/Y], C3 и субституциите [U/X], i, [Y/a].
Когато са изпълнени условията от дефиницията за добре проведен резолвентен процес, ясно е, че при i=1,2,...,n целта Gi е най-обща резолвента на целта Gi-1 и клаузата Ci (изискването Ciў да няма общи променливи с Gs1s2...si-1 е даже в повече, отколкото е нужно за това). Следователно при същите условия целта Gн е най-обща резолвента на целта G и редицата C1, C2, ..., Cn. Последното пък позволява да се докаже с индукция относно n, че добре проведен резолвентен процес за целта G и редицата от клаузи C1, C2, ..., Cn е осъществим винаги, когато тази цел и тази редица от клаузи имат резолвента.
Забележка 2. Когато унификацията на две атомарни формули се извършва по някой от обичайните алгоритми, в случай на успех тя дава унификатор, чието прилагане към произволна безкванторна формула не привнася в резултата нови променливи, неучастващи в поне една от двете атомарни формули. Ако, както обикновено, се използват само такива унификатори, то един прост (макар и малко разточителен) начин за осъществяване на добре проведен резолвентен процес е следният: при избора на варианти на клаузите се грижим допълнително (тук именно е разточителството) променливите на тези варианти винаги да са различни от променливите на първоначалната цел и от променливите на всички варианти, използвани в предходните резолвентни стъпки.
Оеновният резултат за добре проведени резолвентни процеси, който ще установим, е следният.
Теорема. При условията от дефиницията за добре проведен резолвентен процес целта Gs1s2...sn е най-общ частен случай на целта G, имащ проста резолвента с редицата от клаузи C1, C2, ..., Cn.
Доказателство. Нека G0, G1, G2, ..., Gn, C1ў, C2ў, ..., Cnў, s1, s2, ..., sn удовлетворяват условията от дефиницията за добре проведен резолвентен процес за целта G и редицата от клаузи C1, C2, ..., Cn. Използвайки терминологията от предходния въпрос, можем да твърдим, че целта Gn е резолвента на G с C1, C2, ..., Cn при използване на субституции s1, s2, ..., sn. Следователно (по доказаната там теорема за преминаване от резолюция към проста резолюция) Gn е проста резолвента на целта Gs1s2...sn с редицата C1, C2, ..., Cn. И така, частният случай Gs1s2...sn на G има проста резолвента с редицата от клаузи C1, C2, ..., Cn. Да разгледаме сега произволен частен случай G на G, който има проста резолвента със същата редица от клаузи. Ще покажем, че G е частен случай на Gs1s2...sn. Направеното предположение за G означава, че има редица от цели G0, G1, G2, ..., Gn, такава, че G0=G и Gi е проста резолвента на Gi-1 и Ci при i=1,2,...,n. За да докажем, че G е частен случай на Gs1s2...sn, достатъчно е да докажем, че при i=0,1,2,...,n има субституция qi, за която са в сила равенствата
G=Gs1s2...siqi, Gi=Giqi
(желаното заключение ще се получи от този резултат при i=n). Доказателството ще извършим чрез индукция. При i=0 горните две равенства всъщност са равносилни едно с друго, а субституция qi, която ги удовлетворява, съществува поради това, че G е частен случай на G. Сега ще покажем съществуването на субституция qi, удовлетворяваща горните равенства за дадено i измежду 1,2,...,n, при предположение, че някоя субституция qi-1 удовлетворява равенствата
G=Gs1s2...si-1qi-1, Gi-1=Gi-1qi-1.
Тъй като целта Gi е непосредствена резолвента на Gi-1 с някой частен случай на клаузата Ci, а Ci и Ciў имат едни и същи частни случаи, можем да разгледаме такава субституция gi, че Gi да е непосредствена резолвента на Gi-1 с клаузата Ciўgi. Без ограничение на общността можем да считаме, че субституцията gi съвпада със субституцията qi-1 за всички променливи, които не са от множеството VAR(Ciў) - в частност за всички променливи на целта Gi-1 и за всички променливи на целта Gs1s2...si-1. Тогава в предположените две равенства можем да заменим qi-1 с gi, т.е. ще имаме равенствата
G=Gs1s2...si-1gi, Gi-1=Gi-1gi.
Понеже първият член на Gi-1 съвпада с главата на клаузата Ciўgi, второто от горните равенства позволява да твърдим, че gi е унификатор на първия член на Gi-1 и главата на Ciў. Следователно gi=siqi за някоя субституция qi. Това ни дава равенствата
G=Gs1s2...si-1siqi, Gi-1=Gi-1siqi.
По такъв начин вече имаме първото от равенствата, които трябваше да удовлетворява qi. За да получим и второто, ще се възползваме от инвариантността на непосредствената резолюция относно субституции. А именно, от обстоятелството, че Gi е непосредствената резолвента на Gi-1si и Ciўsi, следва, че Giqi е непосредствената резолвента на Gi-1siqi и Ciўsiqi, т.е. на Gi-1 и Ciўgi. Тъй като Gi също е непосредствена резолвента на Gi-1 и Ciўgi, а непосредствената резолвента, когато съществува, е единствена, това показва, че имаме равенството Gi=Giqi, т.е. налице е и второто от двете желани равенства. ї
Последно изменение: 13.06.2002 г.