За крайните редици е дефинирана операция конкатенация, като под конкатенация на две такива редици се разбира редицата, съставена от членовете на първата редица и след тях членовете на втората. Ние ще означаваме конкатенацията като произведение. При този начин на означаване ще бъде в сила например равенството [A,B,C][A]=[A,B,C,A]. Разбира се за всяка цел G ще имаме равенствата

    За една хорнова цел и една хорнова клауза ще казваме, че имат непосредствена резолвента, ако целта не е празна и първият й член съвпада с главата на клаузата. В този случай определяме и какво ще разбираме под непосредствена резолвента на дадената цел с дадената клауза. А именно, непосредствена резолвента на хорновата цел [A|R] с хорновата клауза
        А :- B.
(където разбира се А е атомарна формула, а R и B са хорнови цели) ще наричаме целта BR (очевидно тя се определя еднозначно от дадената хорнова цел и хорнова клауза). Образуването на непосредствена резолвента ще наричаме непосредствена резолюция.

    Пример 1. Нека A₀, A₁, A₂, A₃, A₄ са атомарни формули. Тогава целта [A₀,A₁,A₂] има с клаузите
        A₀ :- A₃, A₂, A₄.
        A₀.
непосредствени резолвенти съответно [A₃,A₂,A₄,A₁,A₂] и [A₁,A₂].

В сила е следното свойство на непосредствената резолюция.

    Инвариантност на непосредствената резолюция относно субституции. Нека една хорнова цел G има с дадена хорнова клауза C непосредствена резолвента Gў и нека s е произволна субституция. Тогава целта s(G) има с клаузата s(C) непосредствена резолвента s(Gў).

    Доказателство. Нека G има вида [A|R], а C - вида
        А :- B.
Тогава Gў е целта BR, а s(G) и s(C) са съответно целта [s(A)|s(R)] и клаузата
        s(А) :- s(B).
Оттук е ясно, че s(G) има със s(C) непосредствена резолвента s(B)s(R) и това е точно целта s(Gў).  _ї

    Случаите, когато една хорнова цел и една хорнова клауза имат непосредствена резолвента, са сравнително редки. Затова ще въведем и две по-общи понятия за резолвента (те ще могат да бъдат от полза  дори и понякога, когато съществува непосредствена резолвента). Първото от тези понятия въвеждаме със следната дефиниция: проста резолвента на дадена хорнова цел с дадена хорнова клауза ще наричаме хорнова клауза, която е непосредствена резолвента на дадената цел с някой частен случай на дадената клауза. Образуването на проста резолвента ще наричаме проста резолюция. Разбира се непосредствените резолвенти са и прости резолвенти, защото всяка хорнова клауза е частен случай на себе си, но обратното не е вярно. Например, ако p е едноместен предикатен символ и a е константа, то празната цел е проста резолвента на целта [p(a)] и на клаузата
        p(X).
Очевидно обаче споменатите цел и клауза нямат непосредствена резолвента. Добре е да отбележим, че за разлика от непосредствената резолвента простата резолвента не винаги е единствена в случаите, когато съществува. В това можем да се убедим, заменяйки в току-що разгледания пример използваната клауза със следната:
        p(X) :- p(Y).
А именно, за всеки терм T целта [p(T)] ще бъде проста резолвента на целта [p(a)] с горната клауза.

    Доказаната преди малко инвариантност на непосредствената резолюция относно субституции има следния частичен аналог за случая на проста резолюция.

    Инвариантност на простата резолюция относно субституции. Нека една хорнова цел G има с дадена хорнова клауза проста резолвента Gў и нека s е произволна субституция. Тогава целта s(G) има със същата клауза проста резолвента s(Gў).

    Доказателство. Да означим споменатата по-горе клауза с C. Целта Gў е непосредствена резолвента на G с някой частен случай K на C. Оттук получаваме, че s(Gў) е непосредствена резолвента на s(G) с клаузата s(K). Последната обаче също е частен случай на C и следователно s(Gў) е проста резолвента на s(G) с C.  _ї

    В сила е следното семантично свойство на простите резолвенти.

    Коректност на простата резолюция между хорнова цел и хорнова клауза. Нека S е структура и е дадена една хорнова клауза, която е тъждествено вярна в S. Всеки път, когато една хорнова цел има проста резолвента с тази клауза и въпросната проста резолвента е изпълнена в S при дадена оценка v на променливите, самата цел също е изпълнена в S при оценката v. Следователно всеки път, когато една хорнова цел има проста резолвента с дадената клауза и въпросната проста резолвента е изпълнена тъждествено в S, самата цел също е изпълнена тъждествено в S.

    Доказателство. Да разгледаме произволна хорнова цел [A|R], която има проста резолвента с дадената клауза. Простата резолвента, за която става дума, е непосредствена резолвента на въпросната цел с някой частен случай на дадената клауза. Той трябва да има вида
        А :- B.
Непосредствената резолвента на разглежданата цел с него пък ще бъде целта BR. Нека тя е изпълнена в S при дадена оценка v на променливите. Тогава в S при оценката v ще бъдат верни всички членове на целта B и всички членове на целта R. Благодарение на тъждествената вярност на дадената клауза в S отбелязаният по-горе неин частен случай също е тъждествено верен в S (поради запазването на тъждествената вярност при преминаване към частен случай). При това положение верността в S на членовете на целта B при оценката v осигурява, че в S при оценката v е вярна и атомарната формула А. В такъв случай обаче в S при оценката v се оказват верни всички членове на целта [A|R].  _ї

    Второто по-общо понятие за резолвента, което е всъщност най-общото, въвеждаме със следната дефиниция: резолвента на дадена хорнова цел с дадена хорнова клауза ще наричаме хорнова цел, която е непосредствена резолвента на някой частен случай на дадената цел с някой частен случай на дадената клауза (или, все едно, проста резолвента на някой частен случай на дадената цел с дадената клауза). Разбира се образуването на резолвента ще наричаме резолюция.

    Пример 2. Нека p и q са двуместни предикатни символи, r е едноместен предикатен символ, a и b са константи. Целта [p(X,b),q(X,Z)] и клаузата
        p(a,X) :- q(X,Z), r(Z).
нямат проста резолвента, защото атомарната формула p(X,b) не е частен случай на атомарната формула p(a,X). Въпреки това те имат резолвента (имат даже безбройно много резолвенти). И наистина, частните случаи на дадената цел са всевъзможните цели от вида [p(T,b),q(T,U)], където T и U са термове, а частните случаи на дадената клауза - клаузите от вида
        p(a,V) :- q(V,W), r(W).
при всевъзможните избори на термове V и W. Ясно е, че един частен случай на целта и един частен случай на клаузата ще имат непосредствена резолвента точно тогава, когато имат съответно вида [p(a,b),q(a,U)] и вида
        p(a,b) :- q(b,W), r(W).
за някой терм U и някой терм W. Оттук виждаме, че резолвенти на дадената цел с дадената клауза са точно целите от вида [q(b,W),r(W),q(a,U)], където W и U са термове. Измежду така описаните резолвенти има най-обща, т.е. такава, на която всички те са частни случаи. В качеството на най-обща резолвента бихме могли да вземем коя да е цел от горния вид, в която термовете W и U са различни помежду си променливи.

    Разбира се съвсем лесно може да се даде и пример на хорнова цел и хорнова клауза, които нямат резолвента и в разглеждания по-общ смисъл. По-интересно е да дадем пример за хорнова цел и хорнова клауза, които имат непосредствена резолвента, но тя не е най-обща измежду техните резолвенти.

    Пример 3. Да разгледаме частния случай [p(a,b),q(a,Z)] на целта от предходния пример и частния случай
        p(a,b) :- q(b,Z),r(Z).
на клаузата от същия пример. Тяхна непосредствена резолвента е целта [q(b,Z),r(Z),q(a,Z)], но съществуват други техни резолвенти, които не са нейни частни случаи. За да се убедим в това, достатъчно е да забележим, че общият вид на резолвентите в настоящия пример е същият както в предходния.

    Като се използва транзитивността на отношението "е частен случай", веднага се вижда, че ако някой частен случай на дадена хорнова цел има резолвента с някой частен случай на дадена хорнова клауза, то всяка резолвента на въпросните частни случаи е резолвента също и на дадената цел с дадената клауза.

    От семантична гледна точка общото понятие за резолвента е полезно благодарение на следващото твърдение.

    Коректност на резолюцията между хорнова цел и хорнова клауза. Нека S е структура и е дадена една хорнова клауза, която е тъждествено вярна в S. Всеки път, когато една хорнова цел има резолвента с тази клауза и въпросната резолвента е изпълнима в S, самата цел също е изпълнима в S.

    Доказателство. Нека е дадена хорнова цел, която има изпълнима в S резолвента с дадената клауза. Въпросната резолвента е изпълнена в S при някоя оценка на променливите и е проста резолвента на някой частен случай на дадената цел с дадената клауза. Доказаното преди малко твърдение за коректност на простата резолюция между хорнова цел и хорнова клауза позволява да заключим, че дадената цел има изпълним в S частен случай. Оттук обаче, както знаем, следва, че и самата дадена цел е изпълнима в S.  _ї

    Следствие 1. Нека P е хорнова програма. Всеки път, когато една хорнова цел има резолвента с някоя клауза от P и въпросната резолвента е изпълнима при P, самата цел също е изпълнима при P.

    Доказателство. Прилагаме доказаното твърдение, като в качеството на S вземем произволен модел за P.  _ї

    Когато е дадена една хорнова програма P, да наречем резолвентна верига, основана на P, такава непразна редица от хорнови цели (крайна или безкрайна), в която всеки член след началния е резолвента на предхождащия го с някоя клауза от P (когато редицата е едночленна, също ще я считаме за резолвентна верига, основана на P). От тази дефиниция и следствие 1 веднага получаваме:

    Следствие 2. Нека P е хорнова програма и нека е дадена една крайна резолвентна верига, основана на P. Ако последният член на въпросната верига е цел, изпълнима при P, то всички членове на веригата са изпълними при P. В частност, ако последен член на веригата е празната цел, то началният член на веригата е изпълним при P.

    Казаното в последното изречение от горното следствие дава един често пъти удобен метод за установяване на изпълнимост на дадена хорнова цел при дадена хорнова програма. Ще го илюстрираме с един пример.

    Пример 4. Нека P е програмата
        p(f(f(X)),f(X)).
        p(X,f(Y)) :- p(X,f(Z)), p(Y,Z).
Ще покажем, че при P е изпълнима целта
        ?- p(U,U).
(т.е. целта [p(U,U)]).Това ще направим, като намерим основана на P резолвентна верига с начален член [p(U,U)] и последен член []. При търсенето на такава верига сме улеснени от обстоятелството, че целта [p(U,U)] няма резолвента с първата клауза на P (защото не съществува атомарна формула, която да е частен случай едновременно на p(U,U) и на p(f(f(X),f(X))). От друга страна атомарната формула p(U,U) има с главата p(X,f(Y)) на втората клауза най-общ унификатор [f(Y),f(Y)=:U,X] и ако приложим тази субституция към целта [p(U,U)] и към втората клауза на P, получаваме цел и клауза, имащи непосредствена резолвента [p(f(Y),f(Z)),p(Y,Z)]. Значи току-що написаната цел е резолвента на [p(U,U)] с втората клауза на P и би могла да бъде взета като следващ член на търсената резолвентна верига. Ако към така избрания член на веригата приложим субституцията [f(Z)=:Y], получаваме цел, която има непосредствена резолвента [p(f(Z),Z)] с подходящ вариант на първата клауза от P. Значи като по-следващ член на търсената верига можем да вземем току-що споменатата непосредствена резолвента. Ако пък към нея приложим субституцията [f(X)=:Z], получаваме цел, която има празна непосредствена резолвента с първата клауза от P. И така, намерихме резолвентната верига относно P с последователни членове

Последно изменение: 4.07.2002 г.
 

Previous  Next  Contents