Друго доказателство за завършване на унификационния процес след краен брой стъпки

    Нека е дадена една система от уравнения от вида
(1) T1=U1, T2=U2, ..., Tn=Un,
където T1, T2, ..., Tn, U1, U2, ..., Un са термове. Да наречем нейна сложност числото (2l+r)2s, където s е броят на неизвестните в нея, относно които тя не е решена, l е сборът на теглата на термовете T1, T2, ..., Tn и r е сборът от теглата на термовете U1, U2, ..., Un. Ще можем да бъдем сигурни в завършването на унификационния процес след краен брой стъпки, ако покажем, че сложността на системата (1) строго намалява винаги, когато извършим някое от преобразуванията премахване на тъждество, разпадане, обръщане и заместване. За първите три от тях това се вижда лесно. За да се убедим, че е така и при четвъртото, първо доказваме, че при всеки избор на променливата X и на термовете U и V теглото на терма [U=:X](V) не надминава произведението от теглата на двата терма U и V (доказателството може да се извърши чрез индукция относно V, съобразена с дефиницията за терм). Да предположим сега, че от системата (1) сме получили нова чрез заместване, основаващо се на наличието в (1) на уравнение X=U, където X е променлива, U е терм, X не е променлива на U и X участва в някое друго от уравненията на (1). Да означим с sў, lў и rў новите стойности, които получават съответно s, l и r след споменатото преобразуване на (1). Тъй като теглото на терма U очевидно е по-малко от сбора 2l+r, лесно се съобразява, че ще бъде в сила неравенството 2lў+rў<(2l+r)2. Оттук, като вземем пред вид и неравенството sўЈs-1, получаваме, че
(2lў+rў)2sў<(2l+r)2sў+1Ј(2l+r)2s.

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