Съдържание 
 

SLD-РЕЗОЛЮЦИЯ

    Нека са дадени едно хорново запитване

?- φ1,φ2,…,φn.
и една положителна хорнова клауза
φ :- ψ1,…,ψm.
В случай, че n>0 и φ1=φ, следното хорново запитване ще наричаме непосредствена SLD-резолвента (или по-кратко непосредствена резолвента) на даденото запитване и дадената клауза:
?- ψ1,…,ψm,φ2, …,φn.
В така дадената дефиниция не се изключват нито възможността числото m да е 0 (т.е. клаузата да бъде с празна предпоставка), нито възможността числото n да е 1 (т.е. запитването да съдържа само атомарната формула φ1). Разбира се, ако m=0, то в непосредствената SLD-резолвента, за която става дума, ще липсва частта ψ1,…,ψm, а ако n=1, то ще липсва частта φ2,…,φn; ако пък имаме едновременно m=0 и n=1, то въпросната непосредствена SLD-резолвента ще бъде празното запитване. Очевидно е, че когато едно хорново запитване и една положителна хорнова клауза имат непосредствена SLD-резолвента, тя е единствена (запитването и клаузата я определят еднозначно). Нейното образуване ще наричаме непосредствена SLD-резолюция.

    Забележка 1. Частта „SLD“ на въведения термин произлиза от английските думи „selection“, „linear“ и „definite“.

    Ролята на непосредствената SLD-резолюция в търсенето на отговори на хорнови запитвания при хорнови програми произтича от следното нейно свойство (вж. доказаното въз основа на него следствие 1)

    Твърдение 1. Нека едно хорново запитване Q и една хорнова клауза C имат непосредствена SLD-резолвента R. Ако клаузата C е в сила в дадена структура S, то всяка субституция, която удовлетворява R в S, удовлетворява и Q в S.

    Доказателство. Да означим с Γ множеството на атомарните формули, които са членове на предпоставката на C, а с Δ  –  множеството на членовете на Q след първия. Нека φ е заключението на C. При направеното предположение за R може да се твърди, че първият член на Q е също φ, а множеството на членовете на R е обединение на множествата Γ и Δ. Ако клаузата C е в сила в дадена структура S, то φ следва в S от множеството Γ, а оттук въз основа на забележка 2 от текста „Субституции, удовлетворяващи дадено множество от атомарни формули в дадена структура“ заключаваме, че всяка субституция, която удовлетворява в S обединението на множествата Γ и Δ, удовлетворява в S също и множеството {φ}∪Δ. То обаче е множеството на членовете на Q. □

    Следствие 1. Нека е дадена една хорнова програма P и нека едно хорново запитване Q има непосредствена SLD-резолвента R с някоя клауза, която е частен случай на клауза от P. Тогава всеки отговор на R при P е отговор и на Q при P,

    Доказателство. Използваме, че частните случаи на клаузите от P са в сила във всеки модел за P. □

    Пример 1. При програмата
a(o,Y,Y).
a(s(X),Y,s(Z)) :- a(X,Y,Z).
m(o,Y,o).
m(s(X),Y,Z) :- m(X,Y,U), a(U,Y,Z).
(от пример 1 във въпроса „Хорнови програми“) ще потърсим отговор на запитването

?- m(s(X),Y,Y), a(X,Y,s(X)).
Това запитване има непосредствена SLD-резолвента с някои частни случаи на последната клауза от програмата, а именно с онези от следния вид, където τ е някой терм:
m(s(X),Y,Y) :- m(X,Y,τ), a(τ,Y,Y).
Съответната непосредствена SLD-резолвента изглежда така:
?- m(X,Y,τ), a(τ,Y,Y), a(X,Y,s(X)).
Ако в качеството на τ вземем константата o, един отговор на въпросната непосредствена SLD-резолвента при разглежданата програма ще бъде субституцията  [X/o, Y/s(o)],  тъй като тя превръща всяка от трите атомарни формули на резолвентата в заключението на някой частен случай на клауза от програмата с празна предпоставка. Според следствие 1 тази субституция е отговор и на първоначалното запитване.

    Възможностите за използване на непосредствена SLD-резолюция по начина, илюстриран чрез горния пример, са обаче доста ограничени. Това се вижда и от обстоятелството, че използваната в примера непосредствена SLD-резолвента

?- m(X,Y,o), a(o,Y,Y), a(X,Y,s(X)).
не притежава от своя страна непосредствена SLD-резолвента с никакъв частен случай на клауза от програмата (посоченият отговор  [X/o, Y/s(o)]  е намерен другояче). Затова ще дефинираме едно по-общо понятие за резолвента.

    Понеже всяко хорново запитване е крайна редица от атомарни формули, дефинирано е какво значи резултат от прилагане на една субституция към дадено хорново запитване. Ако са дадени едно хорново запитване Q, една положителна хорнова клауза C и една субституция σ, то под SLD-резолвента посредством σ (или по-кратко резолвента посредством σ) на Q и C ще разбираме непосредствена SLD-резолвента на частния случай Qσ на Q и някой частен случай на клаузата C. Понякога ще пропускаме уточнението „посредством σ“ и, говорейки за SLD-резолвента на дадено хорново запитване и дадена положителна хорнова клауза, ще имаме пред вид тяхна SLD-резолвента посредством някоя субституция; другояче казано, SLD-резолвентите на запитването и клаузата са непосредствените SLD-резолвенти на частни случаи на запитването и частни случаи на клаузата. Образуването на SLD-резолвента на едно хорново запитване и една положителна хорнова клауза ще наричаме SLD-резолюция.

    Пример 2. Ако дадено хорново запитване Q и някой частен случай на дадена положителна хорнова клауза C имат непосредствена SLD-резолвента R, то R е SLD-резолвента на Q и C посредством тъждествената субституция.

    Пример 3. Запитването

?- m(X,Y,o), a(o,Y,Y), a(X,Y,s(X)).
и третата клауза на програмата от пример 1 имат следната SLD-резолвента посредством субституцията  [X/o] :
?- a(o,Y,Y), a(o,Y,s(o)).
Същото запитване и четвъртата клауза на програмата имат например такива SLD-резолвенти посредством субституцията  [X/s(X)] :
?- m(X,Y,U), a(U,Y,o), a(o,Y,Y), a(s(X),Y,s(s(X))).
?- m(X,Y,V), a(V,Y,o), a(o,Y,Y), a(s(X),Y,s(s(X))).
?- m(X,Y,s(U)), a(s(U),Y,o), a(o,Y,Y), a(s(X),Y,s(s(X))).
?- m(X,Y,o), a(o,Y,o), a(o,Y,Y), a(s(X),Y,s(s(X))).
?- m(X,Y,X), a(X,Y,o), a(o,Y,Y), a(s(X),Y,s(s(X))).
?- m(X,Y,Y), a(Y,Y,o), a(o,Y,Y), a(s(X),Y,s(s(X))).
С първата и с втората клаузи на програмата обаче запитването няма SLD-резолвента.

    Твърдение 1 се обобщава по следния начин.

    Твърдение 2. Нека едно хорново запитване Q и една хорнова клауза C имат SLD-резолвента R посредством дадена субституция σ. Ако клаузата C е в сила в дадена структура S и една субституция σ′ удовлетворява R в S, то субституцията σσ′ удовлетворява Q в S.

    Доказателство. Нека клаузата C е в сила в дадена структура S и дадена субституция σ′ удовлетворява R в S. Запитването R е непосредствена SLD-резолвента на запитването Qσ и някой частен случай на клаузата C. Понеже и той е в сила в S, твърдение 1 позволява да заключим, че субституцията σ′ удовлетворява в S и запитването Qσ. Оттук с помощта на твърдение 1 от текста „Субституции, удовлетворяващи дадено множество от атомарни формули в дадена структура“ получаваме, че субституцията σσ′ удовлетворява Q в S. □

    Следствие 2. Нека е дадена една хорнова програма P и нека едно хорново запитване Q има SLD-резолвента R посредством дадена субституция σ с някоя клауза от P. Тогава за всеки отговор σ′ на R при P субституцията σσ′ е отговор на Q при P,

    Когато е дадена една хорнова програма P, ще наричаме резолвентна редица относно P такава редица от хорнови запитвания (крайна или безкрайна), в която всеки член след началния е SLD-резолвента на предхождащия го и някоя клауза от P. Ако (Q0, Q1, …, Qk) е k+1-членна резолвентна редица относно P, ще наричаме нейна асоциирана редица от субституции такава k-членна редица (σ1, …, σk) от субституции, че Qi е SLD-резолвента посредством σi на Qi-1 и някоя клауза от P при i=1,…,k. Ще докажем следната важна теорема.

    Теорема за коректност на търсенето на отговори чрез SLD-резолюция. Нека P е дадена хорнова програма, (Q0, Q1, …, Qk) е крайна резолвентна редица относно P, имаща за последен член празното запитване, а (σ1, …, σk) е нейна асоциирана редица от субституции. Тогава произведението σ1…σk е отговор на запитването Q0 при програмата P.

    Доказателство. Чрез индукция от i към i-1 ще докажем, че при i=0,1,…,k произведението σi+1…σk е отговор на запитването Qi при програмата P. При i=k това твърдение е вярно, защото всяка субституция (в това число и тъждествената, на която в случая се равнява произведението σi+1…σk) е отговор на празното запитване при програмата P. Да предположим, че за дадено положително цялo число i, ненадминаващо k, твърдението е вярно. Тогава следствие 2 позволява да заключим, че субституцията σi(σi+1…σk) е отговор на запитването Qi-1 при програмата P. Тази субституция обаче е равна на произведението σiσi+1…σk. С това индукцията е проведена и остава само да използваме доказаното твърдение при i=0. □

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

    Доказателство. Използваме забележка 1 от въпроса „Субституции, удовлетворяващи дадено множество от атомарни формули в дадена структура“. □

    Пример 4. Ще приложим доказаната теорема към задачата, с която се занимахме в пример 1. За да избегнем повечето от словесните обяснения, ще записваме между всеки две последователни запитвания, които получаваме, още и субституцията, посредством която сме образували съответната резолвента, а също използвания при образуването й частен случай от клауза на програмата.
?- m(s(X),Y,Y), a(X,Y,s(X)).
 ι
 m(s(X),Y,Y) :- m(X,Y,U), a(U,Y,Y).
?- m(X,Y,U), a(U,Y,Y), a(X,Y,s(X)).
 [X/o, U/o]
 m(o,Y,o).
?- a(o,Y,Y), a(o,Y,s(o)).
 ι
 a(o,Y,Y).
?- a(o,Y,s(o)).
 [Y/s(o)]
 a(o,s(o),s(o)).
?- .
От теоремата следва, че един отговор на първоначалното запитване при разглежданата програма е субституцията ι [X/o, U/o] ι [Y/s(o)], т.е. субституцията [X/o, U/o, Y/s(o)]. Тогава отговор е и субституцията [X/o, Y/s(o)], съвпадаща с намерената върху множеството на променливите на запитването.

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