| Съдържание |
И така, нека Q и C имат SLD-резолвента. Разбира се, тогава редицата от атомарни формули Q не е празна. Да означим с C′ някой вариант на C, на който множеството на променливите няма общи елементи с множеството на променливите на Q (знаем, че такъв вариант може да се намери). Понеже частните случаи на C и C′ са едни и същи, от дефиницията за SLD-резолвента е ясно, че SLD-резолвентите на Q и C са същите както на Q и C′. Следователно Q и C′ имат SLD-резолвента и е достатъчно да докажем, че те имат най-обща SLD-резолвента.
Първо отбелязваме, че всяка SLD-резолвента на Q и C′ е непосредствена SLD-резолвента на частен случай на Q и частен случай на C′, получени чрез прилагане на една и съща субституция. Действително, да разгледаме произволна SLD-резолвента на Q и C′. Тя е непосредствена резолвента на някой частен случай Qσ1 на Q и някой частен случай C′σ2 на C′, където σ1 и σ2 са някакви субституции. Като използваме, че множествата на променливите на Q и C′ нямат общи елементи и са крайни, можем да намерим субституция σ, която съвпада със σ1 за всички променливи на Q и съвпада със σ2 за всички променливи на C′. Такъв избор на субституцията σ осигурява равенствата Qσ1 = Qσ и C′σ2 = C′σ . Значи разглежданата произволна SLD-резолвента на Q и C′ е непосредствена SLD-резолвента на Qσ и C′σ.
Току-що разгледаната субституция σ очевидно е унификатор на първата атомарна формула в редицата Q и на атомарната формула, която е заключение на C′, следователно тези две атомарни формули са унифицируеми и значи имат и най-общ унификатор (даже такъв, който удовлетворява допълнителните условия, отбелязани в текста „Най-общ унификатор на две атомарни формули“). Нека σ° е техен най-общ унификатор. Тогава, разбира се, запитването Qσ° и клаузата C′σ° ще имат непосредствена SLD-резолвента. Да я означим с R°. Ще покажем, че тя е най-обща SLD-резолвента на Q и C′.
Действително, нека Q и C′ изглеждат съответно така:
Забележка. Ако Q е хорново запитване, C е хорнова клауза и C′ е вариант на C, на който множеството на променливите няма общи елементи с множеството на променливите на Q, то Q и C имат SLD-резолвента точно тогава, когато запитването Q не е празно и първият член на Q е унифицируем със заключението на C′. И наистина, по-горе видяхме, че ако Q и C имат SLD-резолвента, то тези условия са изпълнени. От друга страна, ако тези условия са изпълнени и σ е някой унификатор на първия член на Q и заключението на C′, то Qσ и C′σ имат непосредствена SLD-резолвента и тя е SLD-резолвента на Q и C
Последно изменение: 14.04.2009 г.