16
мысалда бірінші қатарлы логикадағы резолюция ережесіне қосымша
мүмкіндіктер қосу қажет екендігін көрсетеді.
Қажетті тұжырымдар берейік.
Анықтама. Ауыстыру деп теңсіздіктер жиыны аталады s={x
1
=t
1
,
x
2
=t
2
,…, x
n
=t
n
},
x
1
,x
2
,…,x
n
– əртүрлі айнымалы, t
1
,t
2
,…,t
n
– терм, t
i
термінде x
i
(1£ i £ n)
айнымалысы жоқ.
Егер s = (x
1
=t
1
,...,x
n
=t
n
), ал F – дизъюнкт, s(F) арқылы дизъюнкті белгілейміз,
F бірқалыпты айнымалыдан шыққан x
1
–ден t1; жəне т.б. x
n
-нен t
n
. Мысал,
егер s={x
1
=f(x
2
), x
2
=c, x
3
=g(x
4
)), F=R(x
1
,x
2
,x
3
)ÚØP(f(x
2
)), онда s(F)=R(f(x
2
), c,
g(x
4
))ÚØP(f(c). Термдер осы сияқты орындалады.
Ыңғайлы болуы үшін бос ауыстыру енгізейік, теңсіздігі жоқ. Бос
ауыстыруды е арқылы белгілейік.
Анықтама. {E
1
,…,E
k
} – литералдар жиыны немесе термдер жиыны
болсын. Подстановка s ауыстыруы осы жиын үшін унификатор деп аталады,
егер s(E
1
)=s(E
2
)=…=s(E
k
). унификацияланған жиын, егер осы жиын үшін
унификатор болса.
Мысал, атомар формулалар жиыны
{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={x
1
=t
1
, x
2
=t
2
,…, x
k
=t
k
} жəне h={y
1
=s
1
, y
2
=s
2
,…,
y
l
=s
l
} – екі теңдеу. x жəне h ауыстыруы қойылады, тізбектелген болса
{x
1
=h(t
1
), x
2
=h(t
2
),…,x
k
=h(t
k
), y
1
=s
1
, y
2
=s
2
,…, y
l
=s
l
} (4)
x
i
=x
i
үшін 1£ i£ k, y
j
=s
j
, егер y
j
Î{x
1
,…, x
k
}, 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
кезкелген ауыстыру үшін шығады.
17
s = {x
1
=t
1
}○{x
2
=t
2
}○…○{x
n
=t
n
} үшін тізбектер тізімі: s = (x
1
=t
1
, x
2
=t
2
,…,
x
n
=t
n
). &s орына дизъюнкт (жəне терм) қойсақ, тізбек x
1
t
1
-ге ауысады, x
2
t
2
-
ге ауысады жəне т.с.с., x
n
t
n
-ге ауысады
Анықтама. Унификатор 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)}.
Унификация алгоритмі
1 Қадам. k=0, M
k
=M, s
k
=e аламыз.
2 Қадам
. Егер М
k
жиыны бір литералдан тұрса, онда s
k
–ны жалпы
унификатор деп алып, жұмысты аяқтау. Басқа жағдайда N
k
жиынын M
k
-ға
байланысты табу.
3 Қадам
. Егер N
k
жиынында v
k
айнымалысы жəне терм t
k
, v
k
– ға кірмейтін
бар болса, онда 4-ке көшеміз, əйтпесе, М жиыны неунификатор жəне
жұмысты аяқтау деген хаттама беру.
4 Қадам
. s
k+1
={v
k
, t
k
}○s
k
–ға s
k+1
–ді қойса, s
k
-дан v
k
t
k
–ға алмасады, жəне v
k
=t
k
теңсіздігі жазылуы мүмкін. M
k
жиыны v
k
=t
k
алмасуы орындалуы шыққан
литералдар жиынын M
k+1
деп қарастырады.
5 Қадам
. k=k+1 деп жəне 2 қадамға өтеді.
М={P(x,f(y)),
P(a,u)}
болсын.
Проиллюстрируем
работу
алгоритиа
унификации на множестве М. алгоритмнің басында s
1
={x=a} табылады,
N
0
={x,a} болғандықтан. M
1
жиыны {P(a,f(y)),P(a,u)}-ге тең. Сосын s
2
={x=a,
u=f(y)} жəне M
2
={P(a,f(u))}-ге ашылады. Себебі M
2
1 литералдан тұрады
жұмысты аяқтайды жəне s
2
береді.
Екінші мысалды қарастырайық. M={P(x,f(y)), P(a,b)} болсын.
Алгоритмнің бірінші қадамыннан s
1
=(x=a) и M
1
={P(a,f(y)), P(a,b)}. 3-ші
қадамның 2-шісінде М жиыны унификацияланбағаны туралы хаттама
жібереді, себебі N
1
={f(y),a} – де айнымалы жоқ.
