Математическая логика и теория алгоритмов

Обязательный курс для студентов 241 группы 4 семестра обучения. Курс читает профессор В. А. Захаров.

Лекционная нагрузка — 50 ч., семинары — 16 ч.

Лекции по курсу математической логики и логического программирования

Лекция 1. Что изучает логика? Логика в информатике. Структура курса. Исторические сведения. Логические парадоксы.

Лекция 2. Классическая логика предикатов первого порядка. Синтаксис. Термы и формулы.Семантика. Интерпретация. Выполнимость формул.

Лекция 3. Выполнимые и общезначимые формулы. Модели. Логическое следование. Проблема общезначимости. Семантические таблицы.

Лекция 4. Подстановки. Табличный вывод. Корректность табличного вывода.

Лекция 5. Полнота табличного вывода. Теорема Левенгейма-Сколема. Теорема компактности Мальцева. Автоматическое доказательство теорем.

Лекция 6. Общая схема метода резолюций. Равносильные формулы. Теорема о равносильной замене. Предваренная нормальная форма. Сколемовская стандартная форма. Системы дизъюнктов.

Лекция 7. Эрбрановские интерпретации. Теорема Эрбрана. Задача унификации.

Лекция 8. Алгоритм унификации.

Лекция 9. Резолютивный вывод. Корректность резолютивного вывода. Применение метода резолюций.

Лекция 10. Полнота резолютивного вывода.

Лекция 11. Стратегии резолютивного вывода. Вычислительные возможности метода резолюций.