ВУЗ:
Составители:
Рубрика:
46
Прежде всего либо σ, либо
σ
ложны в I. Пусть σ ложна в I. Тогда
дизъюнкт C
1
должен содержать более одной переменной, иначе C
1
был бы ложен в I. Следовательно
1
C
′
должен быть истинен в I.
Таким образом, резольвента
21
CCC
′
∨
′
=
истинна в I. Аналогично
можно показать, что если
σ
ложна в I, то
2
C
′
должен быть
истинен в I, а, следовательно, и
21
CCC
′
∨
′
=
должна быть истинна
в I. Теорема доказана.
Определение.
Пусть S -множество дизъюнктов. Резолютивный
вывод
C из S есть такая конечная последовательность C
1
,C
2
,…,C
k
дизъюнктов, что C
k
=C, а каждый C
i
или принадлежит S или
является резольвентой дизъюнктов, предшествующих C
i
.
Если существует вывод C из S , то C (по теореме 10.1) является
логическим следствием S. Кроме того, если C=П, то s
1
&s
2
&…&s
n
-
противоречие. Здесь { s
1
,s
2
,…,s
n
}=S.
Пример 10.5.
},,{ pqqpS ∨= .
Резолютивный вывод:
p
qqp ,∨
,
П
pp,
.
Следовательно
Лpqqp
≡
∨ ))()((
Рассмотренный метод может быть использован для проверки
того, является ли формула G логическим следствием формул
F
1
,…,F
n
.
Для такой проверки необходимо:
1) представить формулу
GF...FF
n21
∧
∧
∧
∧
в виде КНФ, т.е. в
виде конъюнкции элементарных дизъюнкций.
2) Если из множества дизъюнктов
}G,F,,F{S
21
…
=
удалось
вывести П, то G логическое следствие F
1
,…,F
n
, в противном случае
– нет.
Пример 10.6
. Доказать, что r является логическим следствием
формул
p
r
qq
p
,, →→ .
1) Представляем формулы
r
qq
p
→→ , в виде КНФ:
r
q
r
qq
p
q
p
∨=→∨=→ , .
Страницы
- « первая
- ‹ предыдущая
- …
- 44
- 45
- 46
- 47
- 48
- …
- следующая ›
- последняя »
