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

UptoLike

ВУЗ: 

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

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

Рубрика: 

Математическая Логика и Теория Алгоритмов стр. 38 из 64
© 2003 Галуев Геннадий Анатольевич
M
для
'
S . При этом ни L ни L⎤ не находятся ни в
'
S ни в
M
. Таким образом, всякая
интерпретация для
S , которая содержит
M
и L есть модель для S . Это противоречит
тому, что
S не имеет модели, т.е. предположению, что S невыполнимо. Поэтому
'
S должно быть невыполнимо. Следовательно
'
S невыполнимо тогда и только тогда,
когда
S невыполнимо.
Приведем обоснование правила расщепления. Предположим, что
S невыполнимо.
Если
)(
21
VSS
выполнимо, то или
1
S
или
2
S
имеют модель.
)(
21
SS
имеет модель
M
, то
всякая интерпретация для
S , содержащая
)( LL ⎤
есть модель для S , что противоре-
чит предложению о том, что
S не имеет модели (т.е. невыполнимо). Следовательно
)(
21
SS
невыполнимо.
Пусть теперь
)(
21
SS невыполнимо, если
S
выполнимо, то
S
имеет модель
M
. Если
M
содержит )(LL⎤ , то
M
является моделью для
)(
21
SS
. Это противоречит предполо-
жения о том, что
)(
21
SS невыполнимо. Следовательно
S
невыполнимо тогда и только
тогда, когда
21
VSS невыполнимо.
Рассмотренный метод доказательства может быть применен к любой формуле по-
сле ее приведения к конъюнктивной нормальной форме (конъюнкция дизъюнкций).
Общим недостатком методов доказательства невыполнимости множества дизъ-
юнктов, основанных на теореме Эрбрана, является необходимость порождения ос-
новных примеров дизъюнктов, число которых как правило, растет экспоненционально
с увеличением номера
i
уровня множества
i
H констант,
∞
=
...,2,1i .
Метод резолюций
свободен от этого недостатка и не требует порождения множе-
ства основных примеров дизъюнктов. Этот метод предложен Дж.Робинсоном в 1965
году. Основная идея этого метода состоит в том, чтобы проверить содержит ли
S
пус-
той дизъюнкт 0. Если
S
содержит 0, то
S
невыполнимо, в противном случае проверя-
ется, может ли быть получен 0 из
S .
Рассмотрим сначала метод резолюций для доказательства теорем в исчислении
высказываний.
Сформулируем правило резолюций являющееся обобщением правила однолитер-
ных дизъюнктов.
Правило резолюций. Для любых двух дизъюнктов
1
С и
2
С , если существует лите-
ра
1
L в
1
C , контрарная литере
2
L в
2
C , то вычеркнув
1
L и
2
L из
1
C и
2
C соответственно,
построим дизъюнкцию оставшихся дизъюнктов. Построенный таким образом дизъюнкт
есть резольвента
1
С и
2
С .
Рассмотрим пример.
Пусть
PVRС =
1
PVQC =⎤ . Дизъюнкт
1
C имеет литеру
P
, контрарную литере
P⎤
из
2
C . Значит, в соответствии с правилом резолюций из
1
C и
2
C получаем резольвенту
RVQ .
Имеет место следующая теорема.
Т
Т
е
е
о
о
р
р
е
е
м
м
а
а
.
. Пусть даны два дизъюнкта
1
C
и
2
C
. Тогда резольвента C дизъюнктов
1
C и
2
C есть логическое следствие
1
C и
2
C .
Если имеется два единичных дизъюнкта и существует их резольвента, то эта ре-
зольвента есть пустой дизъюнкт 0. Существенным является тот факт, что для невы-
полнимого множества дизъюнктов применениями правила резолюций можно породить
0.
Пусть
S - множество дизъюнктов. Резолютивный вывод C из S есть такая конеч-
ная последовательность
k
CC ...,,
1
дизъюнктов, что каждый
i
C или принадлежит S или
является резольвентом дизъюнктов, предшествующих
i
C и тогда
k
C есть C . Вывод 0
из
S называется опровержением (или доказательством невыполнимости) S .

Страницы