Унификация алгоритмі
1 Қадам. k=0, Mk=M, sk=e аламыз.
2 Қадам. Егер Мk жиыны бір литералдан тұрса, онда sk –ны жалпы унификатор деп алып, жұмысты аяқтау. Басқа жағдайда Nk жиынын Mk-ға байланысты табу.
3 Қадам. Егер Nk жиынында vk айнымалысы және терм tk , vk – ға кірмейтін бар болса, онда 4-ке көшеміз, әйтпесе, М жиыны неунификатор және жұмысты аяқтау деген хаттама беру.
4 Қадам. sk+1={vk, tk}○sk–ға sk+1–ді қойса, sk-дан vk tk –ға алмасады, және vk=tk теңсіздігі жазылуы мүмкін. Mk жиыны vk=tk алмасуы орындалуы шыққан литералдар жиынын Mk+1 деп қарастырады.
5 Қадам. k=k+1 деп және 2 қадамға өтеді.
М={P(x,f(y)), P(a,u)} болсын. Проиллюстрируем работу алгоритиа унификации на множестве М. алгоритмнің басында s1={x=a} табылады, N0={x,a} болғандықтан. M1жиыны {P(a,f(y)),P(a,u)}-ге тең. Сосын s2={x=a, u=f(y)} және M2={P(a,f(u))}-ге ашылады. Себебі M21 литералдан тұрады жұмысты аяқтайдыжәне s2береді.
Екінші мысалды қарастырайық. M={P(x,f(y)), P(a,b)} болсын. Алгоритмнің бірінші қадамыннан s1=(x=a) и M1={P(a,f(y)), P(a,b)}. 3-ші қадамның 2-шісінде М жиыны унификацияланбағаны туралы хаттама жібереді, себебі N1={f(y),a} – де айнымалы жоқ.
4 қадам орындалғанда , Mk жиынында айнымалылардың бірі өшіріледі (vk айнымалысы), және жаңа айнымалы пайда болмайды. Бұл дегеніміз унификация алгоритмі әрқашан жұмысты аяқтайды, себебі 4 қадам шексіз орындала бермейді. Алгоритм 3 қадамда жұмысын аяқтаса, М жиыны унификацияланбаған. Алгоритм 2 қадамда жұмысын аяқтаса, sk – М жиынының унификаторы. Егер sk – жалпы унификатор болса, дәлелдеу қиын, бірақ біз дәлелдеп көрейік.
Теорема 2.Егер М – ақарлы бос емес литералдар. Егер М унификатор, онда алгоритм унификациясы 2 қадамда жұмысын аяқтайды және sk – М жиынының жалпы унификаторы.
Достарыңызбен бөлісу: |
