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

Технологии в информатике меняются очень быстро. Инженер-программист должен осваивать новые информационные технологии каждые 2-5 лет. Однако при этом концептуальные, базисные теоретические основы информационных технологий остаются неизменными.

Математическая логика относится к теоретическому фундаменту, на котором основаны все существующие и будущие информационные технологии. С помощью логики выражаются семантика языков программирования, спецификация программ (что программа делать), выполняется верификация программ (проверяется, делает ли программа в точности то, что от нее ожидают).

Курс состоит из трех частей. Первая часть посвящена базе математической логики – теории двоичных функций. Вторая часть излагает базовые разделы математической логики, наиболее часто применяемые в практике информационных технологий: методы формализации умозаключений, алгоритмы формального логического вывода, аксиоматические теории. Заключительная часть посвящена методам верификации распределенных алгоритмов и систем.

Курс включает в себя лекции и контрольные работы.

Все материалы, необходимые для изучения курса, доступны студентам в электронном виде. Они основываются на книгах Ю.Г. Карпова: "Теория автоматов" и "Model checking. Верификация параллельных и распределенных программных систем". Но мы приветствуем любознательных студентов, жадно изучающих книги по математической логике.

Достаточно знания математики в объеме средней школы. В первом разделе излагается материал из курса "Дискретная математика", в объеме необходимом для уверенного использования его в "Математической логике". Студенты, знакомые с дискретной математикой, могут пропустить этот раздел, сдав контрольные работы.

Модуль 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

В результате изучения дисциплины студент должен:

• знать понятия, определения, термины, методы, алгоритмы, способы решения задач логики высказываний; логики предикатов и соответствующих исчислений.
• уметь оценить сложность алгоритмов, выделить легко и трудноразрешимые задачи, оценить классы задач P и NP.
• овладеть базовыми методами и алгоритмами проверки логического следования, проверки корректности программ, способами определения сложности вычислений и организации эффективных алгоритмов.

ОПК-1 способность использовать базовые знания естественных наук, математики и информатики, основные факты, концепции, принципы теорий, связанных с фундаментальной информатикой и информационными технологиями

ПК-2 способность понимать, совершенствовать и применять современный математический аппарат, фундаментальные концепции и системные методологии, международные и профессиональные стандарты в области информационных технологий

ПК-6 способность эффективно применять базовые математические знания и информационные технологии при решении проектно-технических и прикладных задач, связанных с развитием и использованием информационных технологий