I. Вопрос 7.1
7 Унификация
Унификация. Правила унификации сложных структур.
Определение 19. Подстановка
Θ = {X
1
/t
1
, . . . X
n
/t
n
}
где
(∀i 6= j)X
i
6= X
j
, t
i
6= X
i
.
Определение 20. Применение Θ к формуле или терму F (F Θ ) – Формула или
терм (опр. рекурсивно), где все X
i
заменены на t
i
.
Определение 21. Унификатор – подстановка Θ , для формул F и G, если F Θ =
GΘ.
Определение 22. Угифицирующиеся – формулы, для которых ∃ унификатор.
Смысл унификации – выявлять эквивалентные формулы, которые могут быть при-
ведены одна к другой путем замены переменных.
Если множество унифицируемо, то существует, как правило, не один унификатор
этого множества, а несколько. Среди всех унификаторов данного множества выде-
ляют так называемый наиболее общий унификатор.
Не из лекций:
Пусть η = {x
1
/t
1
, . . . , x
k
/t
k
} и ξ = {y1/s1, . . . , y
l
/s
l
} – две подстанов-
ки. Тогда произведением подстановок η и ξ называется подстановка,
которая получается из последовательности равенств.
{x
1
/ξ(t
1
), . . . , x
k
/ξ(t
k
), y
1
/s
1
, . . . , y
n
/s
n
}
вычеркиванием равенств вида x
i
= x
i
для 1 <= i <= k, y
j
= s
j
, если
y
j
∈ x1, . . . , xk, для 1 <= j <= l.
Для обозначения результата действия подстановки на дизъюнкт мы
применяем префиксную функциональную запись, поэтому произведение
подстановок η и ξ будем обозначать через и η ◦ ξ, подчёркивая тем самым,
что сначала действует η, а потом ξ.
Для любых подстановок η, ξ, ϑ
η ◦ (ξ ◦ ϑ) = (η ◦ ξ) ◦ ϑ
16