Лекции по дискретной математике. Математическая логика. Зарипова Э.Р - 60 стр.

UptoLike

ВУЗ: 

РУДН | Москва

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

Рубрика: 

60
никаких общих переменных. Пусть L
1
и L
2
- две литеры в C
1
и C
2
соответственно. Если L
1
и
2
L имеют общий унификатор
δ
, то
дизъюнкт
(C
1
δ
\ L
1
δ
)
∪
(C
2
δ
\ L
2
δ
)
называется бинарной резольвентой C
1
и C
2
. Литеры L
1
и L
2
называются отрезаемыми литерами.
Пример 14.2.
Пусть )()( xQxPC
1
∨
=
, а )()( xRaPC
2
∨= . Т.к. x
входит в C
1
и C
2
, то заменяем переменную x в C
2
и пусть
)()( yRaPC
2
∨= . Выбираем L
1
=P(x), )(aPL
2
= .Т.к. )(aPL
2
= , то
L
1
и
2
L имеют унификатор
δ
= {a/x}.
Следовательно
)()()}(),({)}({)}({
}))({)}(),(({)})({)}(),(({
)()(
yRaQyRaQyRaQ
aPyRaPaPaQaP
LCLC
2211
∨==∪
=−∪−=
=−∪−
δδδδ
Таким образом Q(a)
∨
R(y) - бинарная резольвента C
1
и C
2
и P(x)
и
)(aP - отрезаемые литеры.
Определение
. Резольвентой дизъюнктов C
1
и C
2
является одна
из следующих резольвент:
1) бинарная резольвента C
1
и C
2
;
2) бинарная резольвента C
1
и склейки C
2
;
3) бинарная резольвента склейки C
1
и C
2
;
4) бинарная резольвента склейки C
1
и склейки C
2
.
Пример 14.3.
Пусть С
1
=З(ч)
∨
З(а(н))
∨
К(п(н)) и
()
(
)
2
() ()CPfga Qb=∨.
Склейка C
1
есть C
1
′
=P(f(y))
∨
R(g(y)). Бинарная резольвента C
1
′
и
C
2
есть R(g(g(a)))
∨
Q(b) и она же есть и резольвента C
1
и C
2
.
Метод резолюций есть правило вывода, которое порождает
резольвенты для множества дизъюнктов. Метод резолюций полон,
что доказывается следующей теоремой.
Теорема.
Множество S дизъюнктов невыполнимо тогда и
только тогда, когда существует вывод пустого дизъюнкта П из S
(без доказательства).
Пример
применения метода резолюций в исчислении

Страницы