Математическая логика
Целью освоения учебной дисциплины является формирование представлений о классической логике и применение ее в информатике.
Описание:
Технологии в информатике меняются очень быстро. Инженер-программист должен осваивать новые информационные технологии каждые 2-5 лет. Однако при этом концептуальные, базисные теоретические основы информационных технологий остаются неизменными.
Математическая логика относится к теоретическому фундаменту, на котором основаны все существующие и будущие информационные технологии. С помощью логики выражаются семантика языков программирования, спецификация программ (что программа делать), выполняется верификация программ (проверяется, делает ли программа в точности то, что от нее ожидают).
Курс состоит из трех частей. Первая часть посвящена базе математической логики – теории двоичных функций. Вторая часть излагает базовые разделы математической логики, наиболее часто применяемые в практике информационных технологий: методы формализации умозаключений, алгоритмы формального логического вывода, аксиоматические теории. Заключительная часть посвящена методам верификации распределенных алгоритмов и систем.
Программа курса:
Модуль 1. Введение в теорию двоичных функций
- Тема 1. Булевы функции
- Тема 2. Нормальные формы представления булевых функций
- Тема 3. Теорема Поста
- Тема 4. Применение булевых функций
- Тема 5. Бинарные решающие диаграммы
- Тема 6. Конечные автоматы и их применение
Модуль 2. Логика высказываний
- Тема 7. Основные понятия логики высказываний
- Тема 8. Логический вывод в логике высказываний
Модуль 3. Логика предикатов
- Тема 9. Основные понятия логики предикатов
- Тема 10. Логический вывод в логике предикатов
Модуль 4. Аксиоматические теории. Исчисление высказываний
- Тема 11. Основные компоненты аксиоматических теорий
- Тема 12. Теорема Геделя о полноте
Модуль 5. Дедуктивная верификация программ
- Тема 13. Программа как преобразователь предикатов
- Тема 14. Индуктивный метод Флойда
Модуль 6. Проверка корректности реагирующих программ
- Тема 15. Темпоральные логики LTL, CTL
- Тема 16. Алгоритм проверки выполнимости для CTL