ТЕОРЕМА ЗА ПЪЛНОТА НА SLD-РЕЗОЛЮЦИЯТА
Знаем как с помощта на SLD-резолюция се търси отговор на хорново запитване при дадена хорнова програма. Знаем също, че винаги, когато по този начин може да бъде намерен отговор, такъв може да бъде намерен и чрез използване на най-общи резолвенти. От това, което сме установили до момента, не се вижда обаче дали не може да се случи да съществува отговор на едно хорново запитване при дадена хорнова програма без да е налице възможност за намиране на такъв с помощта на SLD-резолюция. Сега ще покажем, че това не може да се случи. Ще докажем даже по-силното твърдение, че ако множеството на членовете на едно хорново запитване е изпълнимо във всеки модел за дадена хорнова програма, то на това запитване може да се даде отговор при дадената програма с помощта на SLD-резолюция (както знаем, ако съществува отговор на дадено хорново запитване при дадена хорнова програма, то множеството на членовете на това запитване е изпълнимо във всеки модел за програмата).
Ще докажем следното твърдение.
Теорема за пълнота на SLD-резолюцията. Нека P е дадена хорнова програма, а Q е хорново запитване, на което множеството от членовете е изпълнимо във всеки модел за P. Тогава съществува резолвентна редица относно P, започваща с Q и завършваща с празното запитване.
Доказателство. На първо време ще докажем теоремата при допълнителното предположение, че P и Q са в сигнатура, съдържаща поне една константа. То ще ни позволи да използваме минимален ербранов модел за програмата P. Нека той е S. Благодарение на това, че множеството на членовете на Q е изпълнимо в структурата S, съществува такава оценка v на променливите в нея, че всички членове на Q да бъдат верни в S при оценката v. Да означим със σ такава субституция, че за всяка променлива ξ на запитването Q да имаме равенството v(ξ) = σ(ξ). Лемата за свеждане на вярност при оценка към вярност на затворен частен случай (вж. въпроса „Ербранови структури“) позволява да заключим, че всички членове на запитването Qσ са затворени атомарни формули, верни в структурата S, а знаем, че всяка такава атомарна формула е изводима чрез програмата P. Като използваме това обстоятелство, ще покажем, че съществува резолвентна редица относно P, започваща с Qσ и завършваща с празното запитване, а разполагайки с нея, лесно ще получим и такава редица, за каквато става дума в заключението на теоремата – достатъчно ще бъде да заменим началния член Qσ на редицата с Q.
За нуждите на доказателството да наречем една затворена атомарна формула φ отстранима, ако при всеки избор на естествено число n и на затворени атомарни формули θ1, …, θn някоя крайна редица от запитвания с начален член
?- φ,θ1,…,θn.
е такава, че в нея всеки член след началния е непосредствена SLD-резолвента на предходния му и затворен частен случай на клауза от P, а последният й член е
?- θ1,…,θn.
(съобразява се, че всички запитвания в такава редица трябва да се състоят от затворени атомарни формули). Лесно е да се убедим във верността на следното помощно твърдение: при всеки избор на естествени числа m и n, на отстраними затворени атомарни формули ψ1, …, ψm и на затворени атомарни формули θ1, …, θn някоя крайна редица от запитвания с начален член
?- ψ1,…,ψm,θ1,…,θn.
е такава, че в нея всеки член след началния е непосредствена SLD-резолвента на предходния му и затворен частен случай на клауза от P, а последният й член е
?- θ1,…,θn.
Чрез използване на това помощно твърдение и на индукция, съобразена с дефиницията за изводимост на затворена атомарна формула чрез P, се доказва, че всяка затворена атомарна формула, изводима чрез P, е отстранима, а оттук веднага получаваме желаното заключение, като още веднъж използваме помощното твърдение (този път с n = 0). Споменатото индуктивно доказателство изглежда така: когато атомарната формула φ е заключение на затворен частен случай на клауза от P с празна предпоставка, при всеки избор на затворени атомарни формули θ1, …, θn съответната редица от запитвания ще бъде само от два члена, а ако е налице затворен частен случай
φ :- ψ1,…,ψm.
на клауза от P с непразна предпоставка, в който всяка от атомарните формули ψ1, …, ψm е отстранима, то при всеки избор на затворени атомарни формули θ1, …, θn можем да получим редица от запитвания, каквато се изисква от дефиницията за отстранимост, като вземем редица със свойствата от помощното твърдение и добавим в началото й като нов член запитването
?- φ,θ1,…,θn.
От предположението за наличие на константа в сигнатурата можем да се освободим, като в случай на липса на константа разгледаме P и Q в сигнатура, получена от първоначалната чрез добавяне на една константа. Предположението на теоремата ще бъде изпълнено и ако си служим с модели на P в тази нова сигнатура, тъй че в нея според доказаното ще съществува резолвентна редица относно P, имаща за начален член Q, а за последен – празното запитване. Тогава, както знаем, ще съществува и канонична резолвентна редица относно P със същите начален и последен член. Поне при условие, че използваните при образуването й най-общи унификатори са намерени по разгледания от нас начин, (а всъщност и без това условие) можем да бъдем сигурни, че въпросната канонична резолвентна редица всъщност е в първоначалната сигнатура (грубо казано, при положение, че добавената константа не фигурира нито в клаузите от P, нито в запитването Q, няма как да се окаже. че някой от използваните най-общи унификатори замества някоя променлива с терм, в който фигурира въпросната константа). □
Забележка. За съжаление доказаната теорема за пълнота предполага използване на SLD-резолюцията по начин, по-изчерпателен от онзи, по който тя се използва при изпълнение на хорновите програми в рамките на езика Пролог. Начинът на нейното използване в Пролог е известен под наименованието операционна семантика на Пролог. Когато едно хорново запитване има SLD-резолвента с повече от една клауза на дадена хорнова програма, подлежаща на изпълнение върху него като програма на Пролог, най-напред се прави опит да се достигне до празно запитване, като се мине през SLD-резолвента на даденото запитване с първата от клаузите, с които то има резолвента, а опит за използване на такава резолвента със следваща от тях се прави само при положение, че след краен брой стъпки се установи, че всевъзможните канонични резолвентни редици, използващи резолвентите с предходни клаузи, са краен брой и никоя от тези редици не завършва с празното запитване. Има много случаи, когато този начин на работа не позволява да се стигне до празно запитване въпреки наличието на резолвентна редица, започваща с даденото запитване и завършваща с празното запитване. Прост пример за такова положение на нещата е следният: при нулместни предикатни символи p и q разглеждаме изпълнението на хорновата програма
върху запитването
Да означим горната програма с P, а разглежданото запитване с Q. То има с първата клауза на P резолвента
Нейна резолвента с третата от клаузите е празното запитване и значи относно P съществува резолвентна редица, започваща с Q и завършваща с празното запитване. Операционната семантика на Пролог води обаче до това, че втората резолвентна стъпка се изпълнява не по този начин и вместо с третата клауза на P се образува резолвента с втората от клаузите, отново се получава първоначалното запитване Q и всичко се повтаря отново. Така се получават все по-дълги начала на една безкрайна резолвентна редица и никога не се стига до празно запитване. В конкретния случай можем да избегнем описания проблем, като разменим поредността на клаузите, изпращайки третата преди втората (получената по този начин хорнова програма ще има същите модели, защото подредбата на клаузите не е от значение за моделите). Има обаче и такива случаи на подобна непълнота на операционната семантика на Пролог, при които няма възможност Пролог да намери отговор, както и да пренареждаме клаузите.
Пример. Да предположим, че работим в сигнатура с константи a и b и с двуместен предикатен символ p, и да разгледаме програма P, състояща се от следните три клаузи, но евентуално не в същата последователност:
| p(a,b).
|
| p(X,Y) :- p(Y,X).
|
| p(X,Y) :- p(X,Z), p(Y,Z).
|
(ср. с пример 1 от въпроса „Изводимост на затворена атомарна формула чрез логическа програма. Минимален ербранов модел“). Нека Q е запитването
Следната редица от запитвания е резолвентна редица относно P (образувана е, като се тръгне от запитването Q и последователно се извърши резолюция с третата от гореизброените три клаузи, с втората, с първата, пак с втората и пак с първата):
| ?- p(b,b).
|
| ?- p(b,Z), p(b,Z).
|
| ?- p(Z,b), p(b,Z).
|
| ?- p(b,a).
|
| ?- p(a,b).
|
| ?- .
|
Не е трудно да се убедим обаче, че независимо от последователността, в която се намират в програмата P съставляващите я три клаузи, при нейното изпълнение върху запитването Q операционната семантика на Пролог поражда безкрайна резолвентна редица, тъй че никога не се достига до празно запитване. А именно, ако в P втората от гореизброените три клаузи предхожда третата, то се получава безкрайната редица, на която всеки член е Q, а в противен случай се получава такава безкрайна резолвентна редица, че в нея всеки член след началния има първа формула от вида p(b,ζ), където ζ е някоя променлива. Заслужава отбелязване и обстоятелството, че не би помогнала и замяна на третата от гореизброените три клаузи с клаузата
| p(X,Y) :- p(Y,Z), p(X,Z).
|
(програмата, получена чрез тази замяна, ще има същите модели, защото и подредбата на атомарните формули в предпоставките на клаузите не е от значение за моделите). И в този случай посочената по-горе шестчленна редица от запитвания, започваща с Q и завършваща с празното запитване, ще бъде резолвентна редица, но при изпълнението на програмата върху Q операционната семантика на Пролог отново ще поражда безкрайна резолвентна редица, каквато и да е последователността на трите клаузи.
Последно изменение: 26.04.2010 г.