Пример 1. Нека p е двуместен предикатен символ, f и g са едноместни функционални символи и P е хорновата програма
        p(X,f(X)).
        p(Y,g(Z)).
Нека G е хорновата цел
        ?-  p(U,V), p(V,U).
Тогава следният частен случай на G е тъждествено верен във всеки модел за P:
        ?-  p(g(Z),f(g(Z))), p(f(g(Z)),g(Z)).

    Всеки частен случай на една хорнова цел се получава от нея чрез прилагане на някоя субституция (например току-що разгледаният частен случай на G може да се получи от G чрез прилагане на субституцията [U/g(Z),V/f(g(Z))]). Когато са дадени една хорнова програма P и една хорнова цел G, ще наричаме удовлетворяваща субституция за G при P такава субституция s, че целта Gs да бъде тъждествено вярна във всеки модел за P (следователно субституциятя [U/g(Z),V/f(g(Z))] е една удовлетворяваща субституция за целта G от горния пример при програмата P от същия пример). Ясно е, че за да съществува удовлетворяваща субституция за G при P, необходимо и достатъчно е G да е изпълнима при P. Ние знаем как с помощта на резолюция може да се установява изпълнимостта на една хорнова цел при една хорнова програма. Сега ще покажем как резолюцията може да се използва и за намиране на удовлетворяваща субституция в този случай. За да направим това, ще разгледаме един специален вид резолюция на хорнова цел и хорнова клауза (този вид резолюция ще играе главно спомагателна роля в нашето изложение).

    Ако са дадени една хорнова цел и една хорнова клауза, ние ще наричаме тяхна проста резолвента такава хорнова клауза, която е непосредствена резолвента на дадената цел с някой частен случай на дадената клауза. Образуването на проста резолвента ще наричаме проста резолюция. Разбира се непосредствените резолвенти са и прости резолвенти, защото всяка хорнова клауза е частен случай на себе си, но обратното не е вярно.

    Пример 2. Ако p е едноместен предикатен символ и a е константа, то празната цел е проста резолвента на целта с единствен член p(a) и на клаузата
        p(X).
Очевидно обаче споменатите цел и клауза нямат непосредствена резолвента.

    Добре е да отбележим, че за разлика от непосредствената резолвента простата резолвента не винаги е единствена в случаите, когато съществува. В това можем да се убедим, заменяйки в току-що разгледания пример използваната клауза със следната:
        p(X) :-  p(Y).
А именно, разгледаната преди малко цел и горната клауза ще имат безбройно много прости резолвенти - такава ще бъде всяка цел с единствен член от вида p(T), където T е някакъв терм.

    Забележка 1. Очевидно една хорнова цел е резолвента на дадена хорнова цел G с дадена хорнова клауза C точно тогава, когато е проста резолвента на някой частен случай на G с C.

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

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

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

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

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

    Доказателство. Да разгледаме произволна хорнова цел G, която има проста резолвента Gў с клаузата C. Целта Gў е непосредствена резолвента на G с някой частен случай на C, а той, както знаем, също е клауза, тъждествено вярна в S. Оттук и от свойствата на непосредствените резолвенти следва, че ако Gў е вярна в S при дадена оценка на променливите, то G също е вярна в S при тази оценка. Значи ако Gў е тъждествено вярна в S, то G също е тъждествено вярна в S.  _ї

    Преди известно време ние преминахме от дефиницията за резолвента на хорнова цел и хорнова клауза към дефиниция за резолвента на хорнова цел и редица от хорнови клаузи. Сега ще извършим аналогичен преход за случая на прости резолвенти. А именно, ще казваме, че една хорнова цел Gў е проста резолвента на дадена хорнова цел G и дадена n-членна редица C₁, C₂, ..., C_n от хорнови клаузи, ако съществува такава n+1-членна редица G₀, G₁, G₂, ..., G_n от хорнови цели, че G₀=G, G_n=Gў и G_i е проста резолвента на G_i-1 и C_i при i=1,2,...,n.

    От твърдението за коректност на простата резо;юция между хорнова цел и хорнова клауза (като се вземе пред вид обстоятелството, че празната цел е тъждествено вярна формула) очевидно може да се направи такова заключение:

    Достатъчно условие за тъждествена вярност на хорнова цел във всеки модел за дадена хорнова програма. За да бъде дадена хорнова цел G тъждествено вярна във всеки модел на дадена хорнова програма P, достатъчно е празната цел да бъде проста резолвента на G с някоя крайна редица, на която членовете са клаузи от P.

    Забележка 2. Може да се покаже, че условието от горното твърдение е не само достатъчно, но и необходимо.

    Ще ни е нужна още следната дефиниция във връзка с общото понятие за резолвента на хорнова цел с редица от хорнови клаузи (връзката е ясна от забележка 1): ще казваме, че една хорнова цел Gў е резолвента на дадена хорнова цел G с дадена n-членна редица C₁, C₂, ..., C_n от хорнови клаузи при използване на субституции s₁, s₂, ..., s_n, ако съществува такава n+1-членна редица G₀, G₁, G₂, ..., G_n от хорнови цели, че G₀=G, G_n=Gў и  G_i  е проста резолвента на  G_i-1s_i  и  C_i при i=1,2,...,n. С помощта на така дефинираното понятие ще формулираме следния резултат.

    Теорема за преминаване от резолюция към проста резолюция. Нека една хорнова цел Gў е резолвента на дадена хорнова цел G с дадена n-членна редица C₁, C₂, ..., C_n от хорнови клаузи при използване на субституции s₁, s₂, ..., s_n. Тогава Gў е проста резолвента на целта Gs₁s₂...s_n с редицата C₁, C₂, ..., C_n.

    Доказателство. Разглеждаме n+1-членна редица G₀, G₁, G₂, ..., G_n от хорнови цели със свойството от дефиницията за резолвента при използване на дадени субституции. Като използваме инвариантността на простата резолюция относно субституции, получаваме, че при i=1,2,...,n целта  G_is_i+1...s_n  е проста резолвента на целта  G_i-1s_is_i+1...s_n  с клаузата C_i. При това положение заключението на теоремата се получава от дефиницията за проста резолвента с редица от клаузи, като се разгледа редицата от цели   G₀s₁s₂...s_n,  G₁s₂...s_n,  ...,  G_n-1s_n,  G_n.   _ї

    Следствие. Нека P е хорнова програма, G е хорнова цел и празната цел е резолвента на G с някоя n-членна редица от клаузи на P при използване на субституции s₁, s₂, ..., s_n. Тогава произведението s₁s₂...s_n на тези субституции е удовлетворяваща субституция за G при P.

    Доказателство. Прилагаме теоремата, като вземаме празната цел в качеството на Gў, и използваме достатъчното условие за тъждествена вярност на хорнова цел във всеки модел за дадена хорнова програма.  _ї

    Пример 3. Нека p е двуместен оредикатен символ, a и b са константи, s и u са съответно едноместем и двуместен функционален символ, а P е хорновата програма
        p(X,s(X)).
        p(X,u(A,B)) :–  p(X,A).
        p(X,u(A,B)) :–  p(X,B).
Нека G е целта
        ?-  p(a,Z), p(b,Z).
Лесно се вижда, че празната цел е резолвента на една четиричленна редица от клаузи на P с използване на субституциите [Z/u(A,B)], [A/s(а)], i, [B/s(b)] (последователните членове на споменатата редица от клаузи са втората, първата, третата и пак първата клауза на P). Това позволява да заключим, че субституцията [Z/u(s(a),s(b))] е една удовлетворяваща субституция за G при P.
 

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

Previous  Next  Contents