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

UptoLike

ВУЗ: 

СГАУ | Самара

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

Рубрика: 

13
Р
∨
¬
N
1
∨
¬
N
2
…
∨
¬
N
m
¬
N
1
∨
¬
N
2
…
∨
¬
N
m
=
¬
(N
1
∧
N
2
∧
…
∧
N
m
)
P
←
(N
1
∧
N
2
∧
…
∧
N
m
)
P
←
N
1
, N
2
,…N
m
При представлении дизъюнктов фразами Хорна негативные литералы
соответствуют гипотезам, а позитивный литерал представляет заключение.
Единичный позитивный дизъюнкт представляет некоторый факт, то есть
заключение, не зависящее ни от каких гипотез. Часто задача состоит в том,
что надо проверить некоторую формулу, называемую целью, логически
выведенную из множества правил и фактов. Резолюция является
методом
доказательства от противного: исходя из фактов, правил и отрицания цели,
приходим к противоречию (пустому дизъюнкту).
1.2.4 Правило унификации в логике предикатов.
Правило резолюций предполагает нахождение в дизъюнкте литерала,
контрарного литералу в другом дизъюнкте. Для дизъюнктов логики
высказываний это очень просто. Для дизъюнктов логики предикатов процесс
усложняется, так как дизъюнкты могут
содержать функции, переменные и
константы.
Пример 8. Рассмотрим дизъюнкты:
C
1
: P(y)
∨
Q(y),
C
2
:
¬
P(f(x))
∨
R(x).
Не существует никакого литерала в C
1
, контрарного какому-либо
литералу в C
2
. Однако, если подставить f(a) вместо y в C
1
и a вместо x в C
2
,
то исходные дизъюнкты примут вид:
C
1
’
: P(f(a))
∨
Q(f(a)),
C
2
’
:
¬
P(f(a))
∨
R(a).
Так как P(f(a)) контрарен
¬
P(f(a)), то можно получить резольвенту
C
3
’
: Q(f(a))
∨
R(a).
В общем случае, подставив f(x) вместо y в C
1
, получим
C
1
’’
: P(f(x))
∨
Q(f(x)).
Литерал P(f(x)) в C
1
’’
контрарен литералу
¬
P(f(x)) в C
2
.
Следовательно, можно получить резольвенту
C
3
: Q(f(x))
∨
R(x).
Таким образом, если подставлять подходящие термы вместо
переменных в исходные дизъюнкты, можно порождать новые дизъюнкты.
Отметим, что дизъюнкт C
3
из примера 8 является наиболее общим
дизъюнктом в том смысле, что все другие дизъюнкты, порожденные
правилом резолюции будут частным случаем данного дизъюнкта.
Определение 7: Подстановка
θ
– это конечное множество вида
{t
1
/v
1
,…,t
n
/v
n
}, где каждая v
i
– переменная, каждый t
i
– терм, отличный от v
i
,
все v
i
различны.

Страницы