Логическое программирование на языке Visual Prolog. Солдатова О.П - 14 стр.

UptoLike

ВУЗ: 

СГАУ | Самара

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

Рубрика: 

14
Определение 8: Подстановка
θ
называется унификатором для
множества {E
1
,…, E
k
} тогда и только тогда, когда E
1
θ
=E
2
θ
=… E
k
θ
.
Множество {E
1
,…, E
k
} унифицируемо, если для него существует
унификатор.
Прежде чем применить правило резолюции в исчислении предикатов
переменные в литералах необходимо унифицировать.
Унификация производится при следующих условиях:
1. Если термы константы, то они унифицируемы тогда и только
тогда, когда они совпадают.
2. Если в первом дизъюнкте терм переменная, а во втором
константа, то
они унифицируемы, при этом вместо переменной
подставляется константа.
3. Если терм в первом дизъюнкте переменная и во втором
дизъюнкте терм тоже переменная, то они унифицируемы.
4. Если в первом дизъюнкте терм переменная, а во втором -
употребление функции, то они унифицируемы, при этом вместо
переменной подставляется употребление функции.
5. Унифицируются между собой
термы, стоящие на одинаковых
местах в одинаковых предикатах.
Пример 9. Рассмотрим дизъюнкты:
1. Q(a, b, c) и Q(a, d, l). Дизъюнкты не унифицируемы.
2. Q(a, b, c) и Q(x, y, z). Дизъюнкты унифицируемы. Унификатор - Q(a,
b, c).
Определение 9: Унификатор
σ
для множества {E
1
,…, E
k
} будет
наиболее общим унификатором тогда и только тогда, когда для каждого
унификатора
θ
для этого множества существует такая подстановка
λ
,
что
θ
=
σ
°
λ
, то есть
θ
является композицией подстановок
σ
и
λ
.
Определение 10: Композицией подстановок
σ
и
λ
есть функция
σ
°
λ
,
определяемая следующим образом (
σ
°
λ
) [t]=
σ
[
λ
[t]], где t – терм,
σ
и
λ
-
подстановки, а
λ
[t] – терм, который получается из t путем применения к
нему подстановки
λ
.
Определение 11: Множество рассогласований непустого множества
дизъюнктов {E
1
,…, E
k
} получается путем выявления первой (слева) позиции,
на которой не для всех дизъюнктов из E стоит один и тот же символ, и
выписывания из каждого дизъюнкта терма, который начинается с символа,
занимающего данную позицию. Множество термов и есть множество
рассогласований в E.
Пример 10. Рассмотрим дизъюнкты:
{P(x, f(y, z)), P(x, a), P(x, g(h(k(x))))}.
Множество рассогласований состоит из термов, которые
начинаются
с пятой позиции и представляет собой множество {f(x, y), a,
g(h(k(x)))}.
Алгоритм унификации для нахождения наиболее общего унификатора.

Страницы