Матлог / Matematicheskaya_logika
.pdf
Нормальные формы
Скулемовские функции и приведение формул к скулемовской стандартной форме
Рассмотренный прием удаления квантора существования называется скулемизацией формул, вводимые в процессе скулемизации новые функциональные и предметные символы называются функторами Скулема или скулемовскими функциями.
Сведение проблемы общезначимости формул к проблеме противоречивости систем дизъюнктов
Подстановки и унификация формул
Метод резолюций в логике (исчислении) предикатов
(Если прошлый вопрос есть в билете, то следующая теорема также нужна)
Основная теорема метода резолюций в логике предикатов - теорема полноты резолютивного вывода.
(Если прошлый вопрос есть в билете, то это нужно тоже)
Аксиомы и правила вывода исчисления высказываний
Доказуемость формул
Тождественная истинность выводимых формул.
Теорема Геделя о полноте исчисления высказываний.
Непротиворечивость, полнота и разрешимость исчисления высказываний.
(Если прошлый вопрос есть в билете, то эти 2 следствия также нужны. Если прошлого вопроса нет в билете, то он также нужен для этого вопроса)
Аксиомы и правила вывода исчисления предикатов.
(На всякий случай)