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

Технологии в информатике меняются очень быстро. Инженер-программист должен осваивать новые информационные технологии каждые 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