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

UptoLike

ВУЗ: 

СГАУ | Самара

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

Рубрика: 

15
Пусть E – множество дизъюнктов, D – множество рассогласований, k –
номер итерации, σ
k
наиболее общий унификатор на k-ой итерации.
Шаг 1. Присвоим k=0, σ
k
=e (пустой унификатор), E
k
=E.
Шаг 2. Если для E
k
не существует множества рассогласований D
k
, то
остановка: σ
k
– наиболее общий унификатор для E. Иначе найдем множество
рассогласований D
k
.
Шаг 3. Если существуют такие элементы v
k
и t
k
в D
k
, что v
k
переменная, не входящая в терм t
k
, то перейдем к шагу 4. В противном случае
остановка: E не унифицируемо.
Шаг 4. Пусть σ
k+1
=σ
k
{ t
k
/ v
k
}, заменим во всех дизъюнктах E
k
t
k
на v
k
.
Шаг5. K=k+1. Перейти к шагу 2.
Пример 11. Рассмотрим дизъюнкты:
E={P(f(a), g(x)), P(y, y)}.
1. E
0
=E, k=0,
σ
0
=e.
2. D
0
={f(a),y}, v
0
=y, t
0
=f(a).
3.
σ
1
=={f(a)/y}, E
1
={P(f(a), g(x)), P(f(a), f(a))}.
4. D
1
={g(x),f(a)}.
5. Нет переменной в множестве рассогласований D
1
.
Следовательно, алгоритм унификации завершается, множество E –
не унифицируемо.
1.2.5 Метод резолюций в исчислении предикатов
С помощью унификации можно распространить правило резолюций на
исчисление предикатов. При унификации возникает одна трудность: если
один из термов есть переменная x, а другой терм содержит x, но не сводится
к x, унификация невозможна. Проблема решается путем переименования
переменных таким
образом, чтобы унифицируемые дизъюнкты не содержали
одинаковых переменных.
Определение 12: Если два или более литерала (с одиниковым знаком)
дизъюнкта C имеют наиболее общий унификатор
σ
, то C
σ
- называется
склейкой C.
Пример 12. Рассмотрим дизъюнкты:
Пусть C= P(x)
∨
P(f(y))
∨
¬
Q(x).
Тогда 1 и 2 литералы имеют наиболее общий унификатор
σ
= {f(y)/x}.
Следовательно, C
σ
=P(f(y))
∨
¬
Q(f(y)) есть склейка C.
Определение 13: Пусть C
1
и C
2
– два дизъюнкта, которые не имеют
никаких общих переменных. Пусть L
1
и L
2
- два литерала в C
1
и C
2
соответственно. Если L
1
и
¬
L
2
имеют наиболее общий унификатор
σ
, то
дизъюнкт (C
1
σ
- L
1
σ
)
∪
(C
2
σ
- L
2
σ
) называется резольвентой C
1
и C
2
.
Пример 13. Пусть C
1
= P(x)
∨
Q(x) и C
2
=
¬
P(a)
∨
R(x). Так как x входит в
C
1
и C
2
, то мы заменим переменную в C
2
и пусть C
2
=
¬
P(a)
∨
R(y). Выбираем
L
1
= P(x) и L
2
=
¬
P(a). L
1
и L
2
имеют наиболее общий унификатор
σ
={a/x}.
Следовательно, Q(a)
∨
R(y) – резольвента C
1
и C
2
.

Страницы