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

Расписание на весенний семестр 2021/2021 учебного года:

Время занятий: понедельник 16:45 – 18:10

Первое занятие: 8 февраля

Объявления:
Заключительная лекция состоится 17 мая. 3 и 10 мая лекций не будет.

Финансовая поддержка. Курс проводится при финансовой поддержке Минобрнауки России (грант на создание и развитие МЦМУ МИАН, соглашение № 075-15-2019-1614).

Задачи к курсу (часть 1)
Задачи к курсу (часть 2)

Лектор
Кузнецов Степан Львович

Организации
Московский физико-технический институт (государственный университет), г. Долгопрудный, Московская обл.
Математический институт им. В.А. Стеклова Российской академии наук, г. Москва
Математический центр мирового уровня «Математический институт им. В.А. Стеклова Российской академии наук» (МЦМУ МИАН)