Анықтама. {E1,…,Ek} – литералдар жиыны немесе термдер жиыны болсын. Подстановка s ауыстыруы осы жиын үшін унификатордеп аталады, егер s(E1)=s(E2)=…=s(Ek). унификацияланған жиын, егер осы жиын үшін унификатор болса.
Мысал, атомар формулалар жиыны
{Q(a,x,f(x)), Q(u,у,z)}
унификациялайды {u=a, x=у,z=f(у)}, ал жиын
{R(x,f(x)), R(u,u)}
унификацияланбайды. Расында да, егер х-ті u-ға ауыстырсақ {R(u,f(u), R(u,u)} жиыны шығады.
u=f(u) ауыстыру жасау мүмкін емес, және ол пайдасыз, R(f(u), f(f(u))) және R(f(u), f(u)), формуласына келеді.
Егер жиын унификацияланған болса, онда ереже бойынша осы жиынның бір ғана емес бірнеше унификаторы болады. Берілген барлық унификаторлардың ішінен жалпы унификатор бөліп алуға болады.
Анықтама. Егер x={x1=t1, x2=t2,…, xk=tk} және h={y1=s1, y2=s2,…, yl=sl} – екі теңдеу. x және h ауыстыруы қойылады, тізбектелген болса
{x1=h(t1), x2=h(t2),…,xk=h(tk), y1=s1, y2=s2,…, yl=sl} (4)
xi=xiүшін 1£ i£ k, yj=sj, егер yjÎ{x1,…, xk}, 1 £ j £ l үшін осы теңдеулерді сызамыз..
Нәтижесі үшін дизъюнкттің орнына префиксті функционалді жазуды қоямыз, сондықтан x және h орнына h◦x аламыз, x- ті сосын h-ті сызамыз.
Мысал қарастырайық. x = {x=f(y), z=y, u=g(d)}, h = {x=c, y=z} болсын. Онда теңдіктер тізімі (4) келесі түрде болады
{x=f(y), z=z, u=g(d), x=c, y=z}.
Осы тізбектерден h◦x = {x=f(y), u=g(d), y=z} шығады.
Осы тізбектенассоциативті екенін дәлелдеу қиын емес,сондықтан кезкелген x,h,x үшін x◦(h◦z)=(x◦h)◦z орындалады, және бос ауыстыру көбейтуге қарағанданейтралдыэлементболады.Соңында s◦e=e◦s=s кезкелген ауыстыру үшін шығады.
s = {x1=t1}○{x2=t2}○…○{xn=tn} үшін тізбектер тізімі: s = (x1=t1, x2=t2,…, xn=tn). &s орына дизъюнкт (жәнетерм) қойсақ, тізбек x1 t1-ге ауысады, x2 t2 - ге ауысады және т.с.с., xn tn-ге ауысады
Анықтама. Унификатор s жиындар литералы немесе термдер деп осы жиынның жалпы унификаторы, егер кез келген t унификаторы үшін литералдар жиыны бар, x ауыстыруы былай болады t=x○s.
Мысал, {P(x,f(а), g(z)), P(f(b),y,v)} жиыны үшін жалпы унификатор болып s={x=f(b), y=f(a), v=g(z)} ауыстыруы болады. Егер t орына {x=f(b), y=f(a), z=c, v=g(c)} унификаторын алсақ, онда x={z=c}.
Егер литералдар жиын унификацияған болса, жалпы унификатор бар болады. Бұл тұжырымды параграф соңында дәлелдейміз. Ал қазір жалпы унификаторды табу алгоритмі көрсетейік. Алгоритм унификация алгоритмі деп аталады. Алгоритмді көрсету үшін жиыдар теңдігі қажет.
Анықтама. М – литералдар немесе термдер жиыны. Бірінші сол жақ позициясын бөліп аламыз, ол жерде барлық литералдар бір символдан тұрмайды.Символдан басталатын, сол позицияны алатын әрбір литералдан теңдеу жазып аламыз. (Бұл теңдеу литералдың өзі, атомарлы формула және терм). Теңдеулерден шыққан жиын М –дағы ақылдасқан жиын деп аталады.
Мысал, егер M={P(x, f(y), a), P(x,u, g(y)), P(x, c, v)}, бірінші сол жақ позициясында барлық литералдар бір символдан тұрмайды – бесінші позиция. Ақылдасқан жиын f(y), u, c термдерінен тұрады. Ақылдасқан жиын {P(x, y), ØP(a, g(z))} ол жиын. Егер M={ØP(x, y),ØQ(a, v)}, онда ақылдасқаны мынаған тең: {P(x, y), Q(a, v)}.
Достарыңызбен бөлісу: |