Математическое введение в декларативное программирование. Зюзысов В.М. - 38 стр.

UptoLike

ВУЗ: 

ТГУ | Томск

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

Рубрика: 

Унификатором формул E
1
и E
2
называется такая подстановка θ, что E
1
θ=E
2
θ. Во-
обще говоря, у двух формул E
1
и E
2
может быть бесконечно много унификаторов, однако
среди них всегда имеется наиболее общий (или самый общий) унификатор σ, такой, что
все остальные унификаторы получаются в результате действия на σ некоторыми подста-
новками.
6.8 Правило резолюции для исчисления предикатов
Для применения правила резолюции нужны контрарные литералы в резольвируе-
мых дизъюнктах. Пусть C
1
и C
2
− два дизъюнкта в исчислении предикатов. Правило выво-
да
R
BA
CC
σ
)(
,
21
∨
называется правилом резолюции в исчислении предикатов, если в дизъюнктах C
1
и C
2
су-
ществуют унифицируемые контрарные литералы P
1
и P
2
, то есть C
1
= P
1
∨A, а C
2
= ¬P
2
∨B,
причем атомарные формулы P
1
и P
2
являются унифицируемыми наиболее общим унифи-
катором σ. В этом случае резольвентой дизъюнктов C
1
и C
2
является дизъюнкт (A∨B)σ,
полученный из дизъюнкта A∨B применением унификатора σ.
6.9 Алгоритм резолюций
Мы можем попробовать доказать невыполнимость конечного множества дизъюнк-
тов Γ с помощью следующего алгоритма резолюций ( обозначает пустой дизъюнкт).
while ∉Γ do
begin
выбираем дизъюнкты С и D из Γ, содержащие унифицируемые контрарные литералы; •
•
•
вычисляем резольвенту R;
заменяем Γ на Γ∪{R}.
end
Теорема 12. Если множество дизъюнктов является невыполнимым, то алгоритм
резолюций за конечное число шагов придет к противоречию (пустому дизъюнкту).
В качестве примера проверим невыполнимость множества дизъюнктов
Γ = {P∨Q, P∨R, ¬Q∨¬R, ¬P}.
Дизъюнкты удобно пронумеровать. Получится следующий список:
1. P ∨ Q
2. P ∨ R
3. ¬Q ∨ ¬R
4. ¬P
Затем вычисляются и добавляются к Γ резольвенты. В списке, который приводится
ниже, каждый дизъюнкт − резольвента некоторых из предшествующих дизъюнктов. Но-
мера их приведены в скобках справа от соответствующей резольвенты.
5. P ∨ ¬R (1,3)
6. Q (1,4)
7. P ∨ ¬Q (2,3)
8. R (2,4)
9. P (2,5)
10. ¬R (3,6)
11. ¬Q (3,8)
12. ¬R (4,5)
13. ¬Q (4,7)
14. (4,9)
При работе алгоритма возможны три случая.
38

Страницы