За крайните редици е дефинирана операция конкатенация, като под конкатенация на две такива редици се разбира редицата, съставена от членовете на първата редица и след тях членовете на втората. Ние ще означаваме конкатенацията като произведение. При този начин на означаване ще бъде в сила например равенството [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₂].

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

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

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

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

    Пример 2. Нека p и q са двуместни предикатни символи, r е едноместен предикатен символ, a и b са константи, X и Z са променливи. Целта [p(X,b),q(X,Z)] и клаузата
        p(a,X) :- q(X,Z), r(Z).
очевидно нямат непосредствена резолвента. Въпреки това те имат резолвента (имат даже безбройно много резолвенти). И наистина, частните случаи на дадената цел са всевъзможните цели от вида [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 частен случай. Оттук обаче, както знаем, следва, че и самата дадена цел е изпълнима в 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 с последователни членове

    Забележка 1. При условията на горния пример, щом целта [p(U,U)] е изпълнима при P, значи някой неин частен случай е тъждествено изпълнен при P. Такъв частен случай можем да намерим като, грубо казано, проследим как се изменя термът, който произлиза от променливата U, при последователните извършвани в целите субституции. Въпросното изменение може да бъде описано чрез редицата от термове

    Забележка 2. Посоченият в горната забележка частен случай на целта [p(U,U)] е в съгласие (с точност до преименуване на променливата) с резултата, който дава Strawberry Prolog при изпълнение на програмата от пример 4 върху целта
        ?- p(U,U), write(U).
 

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

Previous  Next  Contents