Описание

Аннотация

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

Для оживления изложения теоретического материала и повышения вовлечённости студентов в курсе используются полезные программные инструменты (например, система интерактивного доказательства теорем Lean и SMT-решатель Z3) и даются упражнения на реализацию алгоритмов математической логики. Писать такие программы удобнее на языке Haskell (или OCaml), хотя другие языки программирования также допускаются.

Цель курса — подготовить студентов к осознанному использованию аппарата математической логики в научных исследованиях и при разработке программного обеспечения в отраслях, где корректность кода оказывается критически важной.

Основные темы курса

Исчисление высказываний.
Логика первого порядка (исчисление предикатов).
Элементы теории моделей и теории доказательств.
Язык Prolog и логическое программирование.
SMT-решатели и их приложения.
Соответствие Карри—Ховарда и методы верификации ПО на его основе.
Темпоральные логики и проверка моделей.
Модальные логики и мультиагентные системы.

Пререквизиты

Дискретная математика
Навыки программирования на языке Haskell (например, в объёме курса Функциональное программирование на языке Haskell) или любом другом языке программирования (менее удобно, но допустимо)

Критерии оценивания

В рамках курса студентам будет предложено выполнить 10 заданий. Каждое задание содержит разные виды упражнений (доказательство, программирование, использование специального инструментария) и оценивается исходя из 10 баллов. Для успешного прохождения курса достаточно набрать 70 баллов.