Математическая логика и теория алгоритмов. Галуев Г.А. - 40 стр.

UptoLike

ВУЗ: 

ТТИ ЮФУ | Таганрог

Составители: 

Рубрика: 

Математическая Логика и Теория Алгоритмов стр. 40 из 64
© 2003 Галуев Геннадий Анатольевич
Где
i
h - переменная,
i
t - терм отличный от
i
h ; все
i
h различны ),,1( ni K= .
Если термы
n
tt ,,
1
K не содержат переменных, то подстановка называется основ-
ной. Подстановка, не содержащая элементов называется пустой и обозначается
ξ
.
Если
E
- выражение и
⎭
⎬
⎫
⎩
⎨
⎧
=Θ
n
n
t
t
γγ
...
1
1
- подстановка, то результат операции под-
становки
),...,(
1 n
tt вместо переменных
n
γ
γ
...,
1
в выражение
E
будем обозначать
Θ
E
, при
этом
ΘE называют примером
E
.
Определение. Пусть
⎭
⎬
⎫
⎩
⎨
⎧
=Θ
n
n
x
t
x
t
,...,
1
1
и
⎭
⎬
⎫
⎩
⎨
⎧
=
m
m
y
u
y
u
,...,
1
1
μ
две подстановки. Тогда
композиция
Θ и
μ
есть подстановка, обозначаемая
ομ
Θ
, которая получается из мно-
жества
⎭
⎬
⎫
⎩
⎨
⎧
m
m
n
n
y
u
y
u
x
t
x
t
,...,,...,
1
1
1
1
μμ
вычеркиванием всех элементов
j
j
x
t
μ
, для которых
jj
xt =
μ
(т.е. исключается подстановка переменной вместо самой себя) и всех элемен-
тов
i
i
y
u
таких, что
{
}
nj
xxy ,,
1
K∈ (исключается неоднозначность подстановки).
Например:
{}(){}
yzxyfxtxt ,,
2211
==Θ
{
} {}
zyybxayuyuyu ,,,,
332211
=
μ
Тогда
(
)
{
}
z
y
y
b
x
a
y
y
x
bf
y
u
y
u
y
u
x
t
x
t
,,,,,,,,
3
3
2
2
1
1
2
2
1
1
=
⎭
⎬
⎫
⎩
⎨
⎧
μμ
Так как
22
xt =
μ
, то
2
2
x
t
μ
(т.е.
y
y
) должно быть вычеркнуто из множества. Так
как
1
y и
2
y содержатся среди
{}
21
, xx , то
1
1
y
u
и
2
2
y
u
должны быть вычеркнуты. В ре-
зультате получаем
()
{
}
z
y
x
bf
,=Θ
μ
o .
Применение метода резолюций требует нахождение подстановки, которая может
сделать несколько выражений тождественными (т.е. унифицировать или склеить вы-
ражения).
Подстановка
Θ
называется унификатором для множества выражений
{}
n
EE ,,
1
K ,
тогда и только тогда, когда
Θ
Θ
Θ
n
EEE ,,,
21
K совпадают между собой. Говорят, что
множество
{}
n
EE ,,
1
K унифицируемо, если для него существует унификатор.
Унификатор
σ
для множества выражений
{
}
n
EE ,,
1
K называется наиболее общим
унификатором, если и только если для каждого унификатора
Θ
для этого множества
существует такая подстановка
μ
, что
μ
σ
o
Θ
.
Приведем алгоритм нахождения наиболее общего унификатора (НОУ) для конеч-
ного унифицируемого множества выражений. Если множество не унифицируемо, то
алгоритм будет этот факт выявлять.
Суть алгоритма заключается в просмотре выражений слева направо, выявлении
первого различия (рассогласования), выделении соответствующих выражений, начи-
нающихся с соответствующих позиций, после чего делается попытка исключения рас-
согласования
и т.д.
Множество рассогласований непустого множества выражений W получается вы-
явлением первой (слева) позиции, на которой не для всех выражений из W стоит
один и тот же символ и затем выписываем из каждого выражения в W подвыражения,
которое начинается с символа, занимающего эту позицию. Множество этих выраже-
ний и будет множеством рассогласований W.
Например
, если
()()
(
)
(
)
(
)
(
)
(
){}
xKhgxPaxPzyfxPW ,,,,,,
=
то множество рассогласова-
ний W есть
() ()()(){}
xKhgazyf ,,,

Страницы