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

UptoLike

ВУЗ: 

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

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

Рубрика: 

Математическая Логика и Теория Алгоритмов стр. 36 из 64
© 2003 Галуев Геннадий Анатольевич
Например:
Пусть
{}
))((),( afPxPS ⎤ . Эрбрановский универсум этого множества
{}
...)),((),(, affafaH = , эрбрановский базис
{
}
)),...((()),((, affPafPaA
=
, полное семан-
тическое дерево имеет вид
)(aP О
)(aP⎤
О О
))(( afP ))(( afP⎤ ))(( afP⎤
))(( afP
О О О О
)))((( affP⎤ )))((( affP
О О
О О
Это дерево имеет конечное замкнутое (закрытое) семантическое дерево вида
)(aP О
)(aP⎤
О О
))(( afP ))(( afP⎤
О О
Поэтому множество
S невыполнимо, а в качестве невыполнимого множества
'
S основных примеров дизъюнктов множества S можно указать
{}
))(()),((),( afPafPaP ⎤⎤ . Легко видеть, что в качестве множества
'
S можно взять также
{}
))(()),(( afPafP ⎤ , конъюнкция которых ложна в любой интерпретации.
Методы доказательства теорем.
Как мы уже отмечали ранее теорема о дедукции в исчислении высказываний
позволяет свести задачу о выводимости некоторой формулы из множества формул
(т.е. задачу доказательства теорем) к задаче о доказательстве общезначимости или
противоречивости пропозиционных форм. Этот же факт как было
показано выше ис-
пользуется и при доказательстве теорем в исчислении предикатов первого порядка.
В соответствии с теоремой Эрбрана для доказательства невыполнимости мно-
жества
S
дизъюнктов достаточно найти конечное невыполнимое множество
'
S основ-
ных примеров дизъюнктов из
S . Так как, основные примеры по определению не за-
висят от переменных, то доказать противоречивость некоторого множества
'
S
основ-
ных примеров можно как и в исчислении высказываний, т.е. путем приведения ис-
ходной конъюнкции дизъюнкций к дизъюнктивной нормальной форме (дизъюнкция
конъюнкций). Однако при использовании такого метода доказательства теорем на-
блюдается экспоненциональный рост числа конъюнкций в неблагоприятных ситуаци-
ях.

Страницы