Математическая логика и теория алгоритмов. Галуев Г.А. - 39 стр.

UptoLike

ВУЗ: 

ТТИ ЮФУ | Таганрог

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

Рубрика: 

Математическая Логика и Теория Алгоритмов стр. 39 из 64
© 2003 Галуев Геннадий Анатольевич
Таким образом, правило резолюций есть правило вывода. Это правило является
обобщением правила
MP
и имеет вид
B
AVBA
⎤,
. Говорят, что дизъюнкт C может быть
выведен или получен из
S , если существует вывод C из S . Вывод может быть пред-
ставлен деревом вывода
, вершина которого – дизъюнкты резолютивного вывода и в
любую вершину заходят только ребра, исходящие из дизъюнктов – посылок правила
резолюций; в дизъюнкты из множества
S ребра не заходят.
Например
дерево вида
О
PVQ О PVQ⎤ О QPV ⎤
О
QPV ⎤⎤
О
Q О Q⎤
О
0
соответствует следующему выводу
1.
PVQ
2.
PVQ⎤ S
3.
QPV ⎤
4.
QPV ⎤⎤
5.
Q из 1 и 2
6.
Q⎤ из 3 и 4
7. 0 из 5 и 6
В случае исчисления предикатов применение метода резолюций осложняется за-
висимостью дизьюнктов от переменных.
Например рассмотрим дизъюнкты:
)())((:
)()(:
2
xVRxfPC
xVQxPС
⎤
здесь не существует никакой литеры в
1
C , контрарной какой-нибудь литеры в
2
C . Однако, если представить
)(af
вместо
X
в
1
C и а вместо
X
в
2
C то получим
))(())((:
'
1
afVQafPC
)())((:
'
2
aVRafPС ⎤
и из
'
1
C и
'
2
C можно уже получить резольвенту
)())((:
'
3
aVRafQC .
Ясно, что получение резольвент из дизъюнктов требует выполнения операций
подстановки.
Подстановкой назовем конечное множество вида:
},,{
11 nn
htht K ,

Страницы