Дәлелдеу.Егер t – М жиынының унификаторы. Индукцией по k индукциясы бойынша дәлелдейміз akбар егер t=ak◦sk.
Индукция базасы: k=0. онда sk=e және ak орнына t алуға болады.
Қадам индукциясы: k мағынасы 0£k£ l теңсіздігінде орындалады десек, ak дегеніміз t=ak○sk.
Егер sl(M) бір литерал құраса, онда алгоритм келесі 2 қадамда тоқтайды. Сонда sl жалпы унификатор болады, себебі t=al○sl.
Егер sl(M) 1 литералдан артық болса. Онда алгоритм унификациясында жиын Nl – теңеседі. al Nl жиынын унифицировать етуі керек, себебі t=al○sl – М жиынының унификаторы. Nl – унификатор ең болмағанда бір v айнымалысы болады.
Егер t – терм Nl-ң ішінен v-ден өте жақсы болса, Множество Nl жиыны al унификатор, сондықтан al(v)=al(t). Бұдан t-ң ішінде v жоқ. 4 қадам алгоритмінде sl+1 –ді алу үшін v=t, т.е. sl+1={v=t}○sl теңдігін қолданған. al(v)=al(t) бұдан al– ң ішінде v=al(t) теңдеуі шығады..
Егер al+1=al\{v=al(t)}. Онда al+1(t)=al(t), t-ңішінде v жоқ. Ары қарай
al+1○{v=t}=al+1È{v=al+1(t)}=al+1È{v=al(t)}=al.
al=al+1○{v=t}. Бұдан,
t=al○sl=al+1○{v=t}○sl=al+1○sl+1.
Кез келген k үшін akбар, t=ak○sk. M жиыны унифицияланған, онда алгоритм2 қадамда жұмысты аяқтау қажет. Сонда соңғы теңдеу sk М жиынының унификаторы, sk(М) жиыны жалпы унификатор, себебі туынды унификатор үшін sk – ға қойылған t бар, ол t=ak○sk.
Теорема дәлелденді.
Достарыңызбен бөлісу: |
