Когато едно хорново запитване и една хорнова клауза имат SLD-резолвента, те, както знаем, имат най-обща SLD-резолвента. Прости примери показват, че тя далеч не винаги е единствена. За да изкажем в малко по-силна форма формулираното по-горе твърдение, ще предположим, че сред крайните резолвентни редици относно P някои са наречени канонични и са изпълнени следните условия: 
      1. Всяка едночленна редица, на която единственият член е някое запитване, е канонична резолвентна редица относно P.
      2. Когато последният член на една канонична резолвентна редица относно P има SLD-резолвента с някоя клауза от P, то, добавяйки като нов последен член подходящо избрана тяхна най-обща SLD-резолвента, получаваме пак канонична резолвентна редица относно P.

    Най-простият начин да се удовлетворят тези две условия по начин, достатъчен за целта, формулирана в първия абзац на настоящия текст, е да се нарекат канонични всички крайни резолвентни редици относно P, в които всеки член след началния е най-обща SLD-резолвента на предхождащия го с някоя клауза от P (бихме могли допълнително да поискаме тази най-обща резолвента да се получава по начина, описан в текста „Най-обща резолвента на хорново запитване и положителна хорнова клауза“, при това с използване на най-общ унификатор, който има допълнителните свойства, отбелязани в текста „Най-общ унификатор на две атомарни формули“). С оглед пък на начина, по който би се изпълнявала програмата P при обичайните софтуерни реализации на езика Пролог, бихме могли да имаме предвид и индуктивен начин на дефиниране на множеството на каноничните резолвентни редици относно P, при който се приемат за негови елементи всички едночленни редици, на които единственият член е някое запитване, и за всяка редица от множеството, последният член на която има SLD-резолвента с някоя клауза от P, се обявява, че елемент на множеството е също и редицата, получена чрез добавяне като нов последен член на избрана по някакво фиксирано правило тяхна най-обща SLD-резолвента).

    В сила е следното твърдение: за всяка резолвентна редица относно P, започваща с Q, съществува такава канонична резолвентна редица относно P, започваща с Q и имаща същия брой членове, че всели член на първата редица е частен случай на съответния член на втората (при това положение е ясно, че ако първата редица завършва с празното запитване, то и втората ще завършва с него).

    За да докажем горното твърдение, да предположим, че (Q₀, Q₁, …, Q_k) е произволна резолвентна редица относно P, започваща с Q. Ще покажем, че за всяко естествено число j, ненадминаващо k, съществува такава канонична резолвентна редица (Q₀°, Q₁°, …, Q_j°) относно P, започваща с Q, че запитването Q_i да бъде частен случай на Q_i° при i=0,1,2,…j (следователно такава канонична резолвентна редица съществува и при j=k). Доказателството ще извършим чрез индукция относно j. При j = 0 в качеството на такава редица вземаме едночленната редица с единствен член Q (тя е канонична резолвентна редица относно P благодарение на условието 1). Да предположим сега, че за някое естествено число j, строго по-малко от k, имаме канонична резолвентна редица (Q₀°, Q₁°, …, Q_j°) относно P с желаните свойства. Членът Q_j+1 на редицата (Q₀, Q₁, …, Q_k) е SLD-резолвента на предхождащия го неин член Q_j с някоя клауза C от P, т.е. Q_j+1 е непосредствена SLD-резолвента на някой частен случай на Q_j с някой частен случай на C. Тъй като Q_j е частен случай на Q_j°, всеки частен случай на Q_j е частен случай и на Q_j°. Следователно Q_j+1 е SLD-резолвента и на Q_j° с C. Щом Q_j° и C имат SLD-резолвента, те (благодарение на условието 2) имат и такава най-обща резолвента Q_j+1°, че редицата (Q₀°, Q₁°, …, Q_j°,Q_j+1°) да бъде канонична резолвентна редица относно P. За да покажем, че и тя има желаните свойства, достатъчно е да покажем, че запитването Q_j+1 е частен случай на Q_j+1°, а това е така, зашото Q_j+1 е една от SLD-резолвентите на Q_j° и C, докато Q_j+1° е тяхна най-обща резолвента.

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