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