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

UptoLike

ВУЗ: 

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

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

Рубрика: 

Математическая Логика и Теория Алгоритмов стр. 35 из 64
© 2003 Галуев Геннадий Анатольевич
Лекция 7
Доказательство теорем в исчислении предикатов.
Теорема Эрбрана.
Перейдем к рассмотрению теорем Эрбрана, которая послужила основой для по-
строения машинных алгоритмов и программ доказательства теоремы. Существуют
два варианта теоремы Эрбрана.
Т
Т
е
е
о
о
р
р
е
е
м
м
а
а
Э
Э
р
р
б
б
р
р
а
а
н
н
а
а
(
(
в
в
а
а
р
р
и
и
а
а
н
н
т
т
1
1
)
)
.
.
Множество дизъюнктов S невыполнимо тогда
и только тогда, когда любому полному семантическому дереву множества
S существу-
ет конечное закрытое дерево.
Доказательство.
Необходимость.
Пусть S невыполнимо и
T
- полное семантическое дерево для
S . Для каждой ветви
B
дерева
T
пусть
B
I
- множество всех литер, приписанных реб-
рам ветви
B
. Тогда
B
I есть интерпретация для
S
. Так как
S
невыполнимо, то
B
I долж-
на опровергать основной пример
'
C некоторого дизъюнкта
C
в
S
(т.е.
'
C должен иметь
значение 0). Однако, т.к.
'
C конечно, то на
B
должен существовать опровергающий
узел
B
N
, лежащий на конечном расстоянии (конечное число ребер в ветви
B
) от
корневого узла дерева
T
. Поскольку каждая ветвь дерева имеет опровергающий
узел, то существует закрытое семантическое дерево
'
T
для S . Далее, т.к. из каждого
узла
'
T
выходит только конечное число ребер, то число ветвей, образованных в де-
реве
'
T
конечно, а следовательно конечно и число вершин (узлов)
'
T
, т.е. полному
семантическому дереву
T
для S соответствует конечное закрытое семантическое де-
рево
'
T
.
Достаточность
. Пусть теперь для каждого полного семантического дерева
T
для
S существует конечное закрытое семантическое дерево
'
T
. Тогда каждая ветвь дере-
ва
T
содержит опровергающий узел. Это означает, что каждая интерпретация опро-
вергает
S . Следовательно, согласно теореме о невыполнимости множества дизъюнк-
тов (см. стр 57), множество дизъюнктов
S
невыполнимо. Теорема доказана.
Приведем теперь второй вариант теоремы Эрбрана
Т
Т
е
е
о
о
р
р
е
е
м
м
а
а
Э
Э
р
р
б
б
р
р
а
а
н
н
а
а
(
(
в
в
а
а
р
р
и
и
а
а
н
н
т
т
2
2
)
)
.
.
Множество дизъюнкторов S невыполнимо то-
гда и только тогда, когда существует конечное невыполнимое множество
'
S основных
примеров дизъюнктов из
S .
Доказательство.
Необходимость.
Пусть
S
невыполнимо и
T
- полное семантическое дерево для
S
. Тогда по теореме Эрбрана (вариант 1) существует конечное закрытое семантиче-
ское дерево
'
T
, соответствующее
T
. Пусть
'
S - множество всех основных примеров
дизъюнктов, которые опровергаются во всех опровергающих узлах
'
T
. Тогда
'
S ко-
нечно, т.к. в
'
T
конечное число опровергающих узлов. Так как
'
S ложно в каждой ин-
терпретации для
'
S , то
'
S - невыполнимо.
Достаточность
. Предположим существует конечное невыполнимое множество
'
S
основных примеров дизъюнктов из S . Так как каждая интерпретация
I
для S со-
держит интерпретацию
'
I
множества
'
S и
'
I
опровергает
'
S , то
I
должна также опро-
вергать
'
S . Однако
'
S опровергается в каждой интерпретации
'
I
, поэтому
'
S опровер-
гается в каждой интерпретации
I
. Следовательно,
'
S
опровергается в каждой интер-
претации
I
множества S . А так как
'
S есть множество основных примеров дизъюнктов
из
S и
'
S опровергается в каждой интерпретации
I
множества S , то множества дизъ-
юнктов
S опровергается в каждой интерпретации для S , а потому невыполнимо. Тео-
рема доказана.

Страницы