Математическая логика и теория алгоритмов — различия между версиями
| Строка 10: | Строка 10: | ||
Лекция 2. '''Классическая логика предикатов первого порядка. Синтаксис. Термы и формулы.Семантика. Интерпретация. Выполнимость формул.''' '''[[Media: Lect241_2.pdf| Лекция 2.]]''' | Лекция 2. '''Классическая логика предикатов первого порядка. Синтаксис. Термы и формулы.Семантика. Интерпретация. Выполнимость формул.''' '''[[Media: Lect241_2.pdf| Лекция 2.]]''' | ||
| − | Лекция 3. '''Выполнимые и общезначимые формулы. Модели. Логическое следование. Проблема общезначимости. Семантические таблицы.''' | + | Лекция 3. '''Выполнимые и общезначимые формулы. Модели. Логическое следование. Проблема общезначимости. Семантические таблицы.''' '''[[Media: Lect241_3.pdf| Лекция 1.]]''' |
| + | |||
| − | Лекция 4. '''Подстановки. Табличный вывод. Корректность табличного вывода.''' | + | Лекция 4. '''Подстановки. Табличный вывод. Корректность табличного вывода.''' '''[[Media: Lect241_4.pdf| Лекция 1.]]''' |
| + | |||
| − | Лекция 5. '''Полнота табличного вывода. Теорема Левенгейма-Сколема. Теорема компактности Мальцева. Автоматическое доказательство теорем.''' | + | Лекция 5. '''Полнота табличного вывода. Теорема Левенгейма-Сколема. Теорема компактности Мальцева. Автоматическое доказательство теорем.''' '''[[Media: Lect241_5.pdf| Лекция 1.]]''' |
| + | |||
Лекция 6. '''Общая схема метода резолюций. Равносильные формулы. Теорема о равносильной замене. Предваренная нормальная форма. Сколемовская стандартная форма. Системы дизъюнктов.''' | Лекция 6. '''Общая схема метода резолюций. Равносильные формулы. Теорема о равносильной замене. Предваренная нормальная форма. Сколемовская стандартная форма. Системы дизъюнктов.''' | ||
Версия 15:11, 24 марта 2016
Обязательный курс для студентов 241 группы 4 семестра обучения. Курс читает профессор В. А. Захаров.
Лекционная нагрузка — 50 ч., семинары — 16 ч.
Лекции по курсу математической логики и логического программирования
Лекция 1. Что изучает логика? Логика в информатике. Структура курса. Исторические сведения. Логические парадоксы. Лекция 1.
Лекция 2. Классическая логика предикатов первого порядка. Синтаксис. Термы и формулы.Семантика. Интерпретация. Выполнимость формул. Лекция 2.
Лекция 3. Выполнимые и общезначимые формулы. Модели. Логическое следование. Проблема общезначимости. Семантические таблицы. Лекция 1.
Лекция 4. Подстановки. Табличный вывод. Корректность табличного вывода. Лекция 1.
Лекция 5. Полнота табличного вывода. Теорема Левенгейма-Сколема. Теорема компактности Мальцева. Автоматическое доказательство теорем. Лекция 1.
Лекция 6. Общая схема метода резолюций. Равносильные формулы. Теорема о равносильной замене. Предваренная нормальная форма. Сколемовская стандартная форма. Системы дизъюнктов.
Лекция 7. Эрбрановские интерпретации. Теорема Эрбрана. Задача унификации.
Лекция 8. Алгоритм унификации.
Лекция 9. Резолютивный вывод. Корректность резолютивного вывода. Применение метода резолюций.
Лекция 10. Полнота резолютивного вывода.
Лекция 11. Стратегии резолютивного вывода. Вычислительные возможности метода резолюций.
Основная литература
- Клини С. Математическая логика. М.:Мир, 1973, 480 с.
- Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. М.:Мир, 1983. 360 с.
- Лавров И.А., Максимова Л.Л. Задачи по теории множеств, математической логике и теории алгоритмов. Москва, "Физико-математическая литература", 1995 г., 250 с.
- Метакидес Г., Нероуд А., Принципы логики и логического программирования. Москва, "Факториал", 1998, 288 с.
Дополнительная литература
- Мендельсон Э. Введение в математическую логику. М.:Наука, 1984. 319 с.
- Верещагин Н.К., Шень А. Языки и исчисления. 2004.
- Успенский В.А., Верещагин Н.К., Плиско В.Е. Вводный курс математической логики. 2004. 128 с.
- Лавров И.А. Математическая логика. Учебное пособие для вузов. М.: Академия, 2006.
- Колмогоров А.Н., Драгалин А.Г. Математическая логика. Серия "Классический университетский учебник". Изд.3, 2006, 240 с.
- Ершов Ю.Л., Палютин Е.А. Математическая логика - М.: 1979.
- Непейвода Н. Н. Прикладная логика. Новосибирск. 2000 г.
