Структурная теория доказательств и алгебраическая логика

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