Научно-исследовательский семинар по математической логике

руководители:

академик РАН
академик РАН Лев Дмитриевич Беклемишев
Алексей Львович Семёнов

проходит по средам 18:30–21:00 в ауд. 16-04 ГЗ МГУ.
Временно заседания проходят через Zoom.

Для получения ссылки (включения в рассылку) напишите
ученому секретарю кафедры / семинара А. Оноприенко
Видеозаписи докладов на YouTube

2021.XX.XX:
Докладчик: Доклад пройдет через Zoom. Для получения ссылки (и включения в рассылку) напишите ученому секретарю семинара Е. Золину.
Видеозапись доклада: YouTube | слайды
Аннотация.

ВЕСНА 2023

2023.04.12: Конференция студентов, аспирантов и молодых учёных «Ломоносов 2023»
1. Долгов Дмитрий Александрович [ тезисы ]
  (Казанский (Приволжский) федеральный университет, научный руководитель — Ишмухаметов Шамиль Талгатович)
  О новом 𝑘-арном алгоритме вычисления НОД
2. Кирова Валерия Орлановна [ тезисы ]
  (МГУ, научный руководитель — Канель-Белов Алексей Яковлевич)
  Two-coloring of R with an arbitrary norm without monochromatic isometric copies of unit arithmetic progressions
3. Машкова Ольга Анатольевна [ тезисы ]
  (МГУ, научный руководитель — Любецкий Василий Александрович)
  Сохранение генов в эволюционном развитии видов на основе гомологичности и локальной синтении
4. Golafshan Mohammadmehdi [ тезисы ]
  (МФТИ, научный руководитель — Канель-Белов Алексей Яковлевич)
  The arithmetic and complexity function of the most significant digits of 𝛼^𝑛
ОСЕНЬ 2022
2022.09.07: Совместная логика задач и высказываний
Докладчик: Оноприенко Анастасия Александровна (асп. 4-го года обучения, науч. рук. Л.Д. Беклемишев)
Аннотация. Интуиционистское направление в математике начало складываться в начале XX века и было связано с кризисом в основаниях математики на рубеже XIX–XX веков. Оно возникло в работах Л. Э. Я. Брауэра и позднее изучалось большим количеством исследователей. Однако ограничение сферы действия закона исключённого третьего, предложенного Л. Э. Я. Брауэром, значительно сокращало количество способов рассуждения, традиционно используемых в математике, и потому вызвало резкую оппозицию со стороны Д.Гильберта. А. Н. Колмогоров предложил истолкование интуиционистского исчисления в рамках стандартных математических понятий. По его замыслу, интуиционистская математика укладывается в рамки классической, если интерпретировать высказывания интуиционистской логики как задачи. В комментарии к своим избранным трудам А. Н. Колмогоров отмечает, что его работа «писалась в надежде на то, что логика решения задач сделается со временем постоянным разделом курса логики. Предполагалось создание единого логического аппарата, имеющего дело с объектами двух типов — высказываниями и задачами».
С. А. Мелиховым была введена в рассмотрение совместная логика задач и высказываний QHC. В логике QHC каждая формула имеет один из двух сортов: высказывание либо задача. Формулы сорта высказывание представляют собой «классическую часть» логики QHC — а именно, для них выполнены все законы классической логики. Формулы сорта задача представляют собой «интуиционистскую часть» логики QHC — для них выполнены все законы интуиционистской логики. Формулы сорта высказывание и сорта задача в логике QHC связаны между собой двумя модальностями ? и !, меняющими сорт формул.
В докладе будет дан обзор основных результатов диссертационной работы докладчика, касающейся совместной логики задач и высказываний QHC. Подробно изучены различные варианты семантики пропозиционального фрагмента логики QHC - логики HC: алгебраическая семантика, реляционная семантика, топологическая семантика. Для всех представленных в работе классов моделей имеет место теорема о полноте и свойство конечных моделей (тем самым установлена разрешимость логики HC). Получен ответ на вопрос, поставленный С. А. Мелиховым, о соотношении ED-принципа и PC-правила. Построена семантика типа Крипке логики QHC и доказана теорема о сильной полноте этой логики относительно предлагаемой семантики. Установлено, что логика QHC является консервативным расширением интуиционистской модальной логики QH4. Доказаны дизъюнктивное и экзистенциальное свойства логики QHC (для формул сорта задача).

ВЕСНА 2022

2022.04.27: Научная конференция «Ломоносовские чтения 2022»
Доклады:
1. О преобразовании протоколов Мерлина–Артура в протоколы Артура–Мерлина.
  Докладчик: проф. Н. К. Верещагин.
2. О полноте модальных логик предикатов.
  Докладчик: проф. В. Б. Шехтман.
2022.04.20: Конференция студентов, аспирантов и молодых учёных «Ломоносов 2022»
1. Константиновский Борис Олегович [ тезисы ]
  (МГУ, научный руководитель — М.Р.Пентус)
  Вложение атомарной теории подмножеств свободных полугрупп в атомарную теорию подмножеств свободных моноидов
2. Машкова Ольга Анатольевна [ тезисы ]
  (МГУ, научный руководитель — В.А.Любецкий)
  Алгоритмическая модель аттенюаторной регуляции
3. Новиков Владислав Викторович [ тезисы ]
  (МГУ, научный руководитель — В.А.Любецкий)
  Линейной сложности алгоритм кратчайшего преобразования циклических графов с произвольными ценами операций
4. Пшеницын Тихон Григорьевич [ тезисы ]
  (МГУ, научный руководитель — М.Р.Пентус)
  Displacement Calculus и гиперграфовое исчисление Ламбека
2022.04.13: Конференция студентов, аспирантов и молодых учёных «Ломоносов 2022»
1. Golafshan Mohammadmehdi [ тезисы ]
  (МФТИ, научный руководитель — А.Я.Канель-Белов)
  The complexity function of leading digits a natural numbers in arbitrary bases
2. Junhu Guo [ тезисы ]
  (Peking university, научный руководитель — А.Жеглов)
  On some questions around Berest's conjecture
3. Гайтимиров Ильяс Ризванович [ тезисы ]
  (Чеченский государственный университет, научный руководитель — С.Х.Алихаджиев)
  Бесконечность - не предел
4. Кирова Валерия Орлановна [ тезисы ]
  (МГУ, научный руководитель — А.Я.Канель-Белов)
  The chromatic number of space with Chebyshev metric without long monochromatic unit arithmetic progressions

ОСЕНЬ 2021

2021.09.08: Предикаты доказуемости и связанные с ними алгебры
Докладчик: Колмаков Евгений Александрович (асп. 4-го года обучения, науч. рук. Л.Д. Беклемишев) 
Видеозапись доклада: YouTube | Слайды
Аннотация. Изучение понятия доказуемости в формальных теориях является одной из центральных задач такого раздела математической логики, как теория доказательств. Фундаментальная работа К. Гёделя, содержащая знаменитые теоремы о неполноте формальных систем, послужила отправной точкой для анализа самого понятия доказуемости формальными методами и привела к возникновению целого спектра направлений для дальнейших исследований. В докладе будет дан обзор основных результатов диссертационной работы докладчика, в которой рассматривается ряд взаимосвязанных вопросов, касающихся формализованного понятия доказуемости в арифметических теориях и относящихся к следующим направлениям.
Во-первых, рассматривается понятие доказуемой n-доказуемости, являющееся вариацией одного из важных сильных понятий доказуемости. В отличие от множества всех n-доказуемых формул, т.е. доказуемых в обычном смысле в данной теории, расширенной множеством всех истинных Π_n-предложений, совокупность формул, утверждение об n-доказуемости которых может быть доказано средствами некоторой перечислимой метатеории, образует перечислимую теорию. В работе найдены естественные рекурсивные аксиоматизации таких теорий в терминах итерированных схем локальной рефлексии, что позволило установить ряд свойств введенных теорий. Помимо этого исследуется вопрос об ускорении доказательств для исходных аксиоматизаций этих теорий по отношению к найденным.
Во-вторых, вводятся новые варианты принципов, выражающих корректность данной теории, а именно, схемы рефлексии с определимыми параметрами, и устанавливается их соотношение с известными формами рефлексии. На этой основе дается новое теоретико-модельное доказательство результата о консервативности между схемами равномерной и локальной рефлексии. Кроме того, исследуется естественным образом возникший вопрос о теоретико-доказательственной силе так называемой теоремы Фефермана, связанной с понятием 1-доказуемости и схемой локальной рефлексии.
В-третьих, изучаются вопросы изоморфизма алгебр доказуемости формальных теорий. Как известно, предикат доказуемости данной арифметической теории индуцирует на булевой алгебре Линденбаума этой теории некоторый унарный оператор, что приводит к понятию алгебры доказуемости данной теории. В работе усиливается знаменитый результат В.Ю. Шаврукова, дающий достаточное условие неизоморфизма алгебр доказуемости для пары арифметических теорий. Полученное усиление позволяет построить ряд новых интересных примеров пар теорий с неизоморфными алгебрами доказуемости.

ВЕСНА 2021

2021.05.12: On axiomatisations and proof theory for Kleene algebra (and friends)
Speaker: Anupam Das (University of Birmingham).
Video: YouTube | Slides
Abstract. Kleene algebra (KA) is a quasi-equational theory that captures the theory of rational language inclusion. However, completeness of the former for the latter is a non-trivial result, finally demonstrated in the celebrated works of Kozen '91 and Krob '91.
In this talk I will speak about a recent line of work that connects cyclic proofs to KA and certain extensions. I will show how a natural non-wellfounded system can be made regular via enriching the syntax of usual sequents to a form of 'hypersequent'. This takes advantage of several basic techniques on the cyclic proof side as well as known normal forms from automaton theory.
As an application, I will explain how to recover an alternative demonstration of Kozen's and Krob's result, as well as a later strengthening to so-called 'left-handed' KAs, due to Boffa '95 (cf. also Kozen & Silva '12).
[1] Dexter Kozen. A completeness theorem for Kleene algebras and the algebra of regular events. LICS 1991.
[2] M. Boffa. Une condition impliquant toutes les identites rationnelles. Theoretical Informatics and Applications 29(6), 515-518, 1995. (in French)
[3] Dexter Kozen, Alexandra Silva. Left-handed completeness. RAMICS 2012.
2021.04.28: Научная конференция «Ломоносовские чтения 2021»
Видеозапись: YouTube
Доклады (в порядке выступления):
1. Количество общей информации в бесконечных двоичных последовательностях [ слайды ]
  Докладчик: проф. Н. К. Верещагин.
2. Теория определимости. Новые подходы и задачи [ слайды ]
  Докладчик: акад. А.Л. Семёнов совместно с С.Ф. Сопруновым.
3. Добавление необходимости к модальным логикам [ слайды ]
  Докладчик: проф. В. Б. Шехтман.
4. Сильная полнота модальных логик относительно конечных шкал [ слайды | видео ]
  Докладчик: с.н.с. Е. Е. Золин.
2021.04.21: Конференция студентов, аспирантов и молодых учёных «Ломоносов 2021»
Видеозапись: YouTube
1. Байрамян Арман Артурович [ тезисы ]
  (ЕрГУ, бакалавриат, науч. руководитель — В.С. Атебекян)
  О независимых системах определяющих соотношений групп периода 3
2. Зверева Татьяна Юрьевна [ тезисы ]
  (СибФУ, магистратура, научный руководитель — к.ф.-м.н. С. И. Башмаков)
  Свойства фреймов и вопросы аксиоматизации линейной ступенчатой логики знания с универсальной модальностью LTK.sl_U
3. Коновалов Александр Юрьевич [ тезисы | слайды ]
  (МГУ, к.ф.-м.н. научный руководитель — доц. В. Е. Плиско)
  Некорректность базисной логики предикатов относительно сильного варианта строгой примитивно-рекурсивной реализуемости
2021.04.14: Конференция студентов, аспирантов и молодых учёных «Ломоносов 2021»
Видеозапись: YouTube
1. Вишникин Максим Евгеньевич [ тезисы ]
  (МГУ, студент, 6 курс, научый руководитель — С. Л. Кузнецов)
  Базовые категориальные грамматики с однозначным присвоением типов
2. Пшеницын Тихон Григорьевич [ тезисы ]
  (МГУ, студент, 4 курс, научый руководитель — М. Р. Пентус)
  Исчисление Ламбека с операциями следования и предшествования
3. Решетников Иван Андреевич [ тезисы ]
  (МФТИ, аспирант, научый руководитель — А. Я. Белов)
  Перекладывания отрезков и фактординамика
4. Рубаненко Евгений Максимович [ тезисы ]
  (МФТИ, студент, научый руководитель — А. Я. Белов)
  О 3-ей проблеме Рестиво-Салеми
2021.04.07: Пороговые функции и пороговые схемы
Докладчик: Подольский Владимир Владимирович, ФКН ВШЭ, МИАН.
Видеозапись доклада: YouTube | Слайды
Аннотация. Исследование пороговых функций и пороговых схем началось с 1960-х годов в связи с ранними работами по искусственному интеллекту. Сейчас эти объекты остаются актуальными в связи с вопросами сложности булевых схем, современной теории обучения и дискретной геометрии. В докладе будет дан обзор некоторых недавних результатов в этом направлении. Если останется время, будет также рассказано о гиперграфовых программах, их вычислительной способности и их приложениях к задаче поиска ответов на запросы к базам данных с онтологическим доступом.
Доклад основан на результатах, вошедших в диссертационную работу докладчика: автореферат.
2020.03.31: Протоколы на популяциях и вычислительная сложность
Докладчик: Раскин Михаил Александрович, Технический университет Мюнхена (TUM)
Видеозапись доклада: YouTube | Слайды
Аннотация. Протоколы на популяциях — модель вычислений, введённая в 2004 году Dana Angluin. В этой модели рассматривается большой набор идентичных агентов с фиксированным размером памяти у каждого; время от времени выбирается пара агентов, которые сообщают друг другу своё состояние и на основании этого одновременно меняют состояние. С одной стороны, протоколы в этой модели можно реализовать даже при весьма ограниченных ресурсах; с другой стороны, такие протоколы достаточны, скажем, для коллективной проверки утверждений об исходной конфигурации, выразимых в арифметике Пресбургера (сложение и порядок целых чисел).
Важным вопросом является сложность проверки свойств таких протоколов, как в общем случае, так и для ограниченных подклассов протоколов. Протоколы на популяциях связаны с сетями Петри, поэтому недавняя неэлементарная нижняя оценка на сложность достижимости в сетях Петри автоматически порождает некоторые нижние оценки для общего случая. В докладе будут приведены результаты о вычислительной сложности разных вопросов о протоколах на популяциях, часть из которых получена докладчиком.
2021.03.17: Схемы для функции голосования и других пороговых функций
Докладчик: Козачинский Александр Николаевич (University of Warwick, выпускник нашей кафедры)
Видеозапись доклада: YouTube | Слайды
Аннотация. Наша работа мотивирована следующим вопросом. Пусть некоторую монотонную булеву функцию можно вычислить схемой полиномиального размера в стандартном полном базисе (состоящем из конъюнкции, дизъюнкции и отрицания). Можно ли тогда эту функцию вычислить схемой полиномиального размера в монотонном базисе (состоящим только из конъюнкции и дизъюнкции)?
Этот вопрос был чрезвычайно актуален после того, как Разборов (1985) показал, что некоторая монотонная булева функция из класса NP не может быть вычислена схемой полиномиального размера в монотонном базисе. Если бы наличие схемы полиномиального размера в стандартном полном базисе влекло наличие схемы полиномиального размера в монотонном базисе (для монотонных функций), то из результата Разборова вытекало бы, что P не равно NP! Однако Разборов же (позже в 1985) доказал, что одно не всегда влечет другое, так что доказать неравенство P и NP таким способом не получится.
Вместо монотонных функций мы рассмотрели аналогичный вопрос для класса самодвойственных функций (т.е. функций, принимающих противоположные значения в противоположных точках булева куба), и там ситуация оказалась противоположной. Стандартный базис для этого класса состоит из функции голосования от 3 переменных и отрицания. Мы показали, что если самодвойственная функция имеет схему полиномиального размера в стандартном полном базисе, то эта функция имеет и схему полиномиального размера в стандартном самодвойственном базисе. Доказан также аналогичный результат о переходе от схем в монотонном базисе к схемам в базисе, состоящим из одной лишь функции голосования от 3 переменных (для функций, являющимися одновременно монотонными и самодвойственными). Отметим, что эти результаты верны не только для размера, но и для глубины схем.
Мы применяем наш результат к функции голосования от n переменных при нечетном n (это функция монотонна и самодвойственна). Для этой функции давно известна явная конструкция схемы логарифмической по n глубины в монотонном базисе. Благодаря нашему результату отсюда извлекается явная схема логарифмической по n глубины, состоящая только из функций голосования от 3 переменных. У этого результата имеются следствия в области протоколов конфиденциального вычисления (Кохен и др. 2013). Для схем, состоящих только из функций голосования от 3 переменных, ранее была известна лишь неявная конструкция (Вэлиент, 1984).
Помимо функции голосования, мы изучаем также другие пороговые функции, получая для них усиления известных результатов. Здесь вместо теорем о переходе от одних схем к другим нам потребовались другие технические инструменты, а именно коммуникационная сложность. Мы получили новый результат о переходе от коммуникационных протоколов к булевым схемам, обобщающий известный результат Карчмера и Вигдерсона (1991).
По совместной работе с В. Подольским (ССС 2020)

ОСЕНЬ 2020

2020.11.18: Конференция студентов, аспирантов и молодых учёных «Ломоносов 2020»
Видеозапись: YouTube
Доклады аспиранов и молодых ученых:
1. Кирова Валерия Орлановна [ тезисы ]
  (МГУ, асп. 2 года, научный руководитель — проф. В. А. Любецкий)
  Алгоритм кратчайшего приведения циклических графов к финальному виду
2. Колмаков Евгений Александрович [ тезисы | слайды ]
  (МГУ, асп. 4 года, научный руководитель — акад. РАН Л. Д. Беклемишев)
  Об изоморфизмах алгебр доказуемости формальных теорий
3. Коновалов Александр Юрьевич [ тезисы | слайды ]
  (МГУ, к.ф.-м.н. научный руководитель — доц. В. Е. Плиско)
  V-реализуемость и интуиционистская логика
4. Оноприенко Анастасия Александровна [ тезисы | слайды ]
  (МГУ, асп. 3 года, научный руководитель — акад. РАН Л. Д. Беклемишев)
  Предикатный вариант объединённой логики задач и высказываний
2020.11.11: Конференция студентов, аспирантов и молодых учёных «Ломоносов 2020»
Видеозапись: YouTube
Доклады студентов:
1. Зверева Татьяна Юрьевна [ тезисы | слайды ]
  (СибФУ, магистратура, научный руководитель — к.ф.-м.н. С. И. Башмаков)
  Унификация и финитная аппроксимируемость линейной ступенчатой логики знания с универсальной модальностью LTK.sl_U
2. Исаев Роман Дмитриевич [ тезисы ]
  (МГУ, студент, научный руководитель — Алексей Яковлевич Канель-Белов)
  Полная система инвариантов многомерного кубика Рубика
3. Мельников Игорь Александрович [ тезисы ]
  (МФТИ, бакалавриат, научный руководитель — проф. А. Я. Канель-Белов)
  О логарифмической оценке функции ко-роста алгебр и равномерно рекуррентных слов
4. Пшеницын Тихон Григорьевич [ тезисы | слайды ]
  (МГУ, 4 курс, научный руководитель — проф. М. Р. Пентус)
  Последовательное замыкание классов языков относительно пересечения и гомоморфизмов
2020.10.21: Научная конференция «Ломоносовские чтения 2020»
Видеозапись: YouTube
Доклады:
1. Модальные логики с оператором транзитивного замыкания [ слайды | видео ]
  Докладчик: с.н.с. Е. Е. Золин.
2. О модальных логиках деревьев [ слайды ]
  Докладчик: проф. В. Б. Шехтман.

ВЕСНА 2020

2020.05.20: О логарифмической оценке функции ко-роста равномерно рекуррентных сверхслов
Докладчик: Мельников Игорь Александрович (МФТИ)
Соавтор: Митрофанов Иван Викторович (Высшая нормальная школа, Париж, Франция)
Видеозапись доклада: YouTube
Аннотация. Бесконечное слово (сверхслово) A называется равномерно рекуррентным (почти периодическим), если для всякого его подслова S существует n, такое что S входит в любой отрезок длины n сверхслова A.
Обструкцией назовем слово, не являющееся подсловом в A, всякое подслово которого уже является подсловом A.
Мы покажем [1], что количество обструкций длины не более n в равномерно рекуррентном слове не меньше log₃n.
[1] Igor Melnikov and Ivan Mitrofanov. On cogrowth function of uniformly recurrent sequences. 2020. https://arxiv.org/abs/2001.02272
2020.04.22: Coq: построение и проверка математических доказательств на компьютере
Докладчик: Кузнецов Степан Львович (МГУ, МИАН, ВШЭ)
Видеозапись доклада: YouTube | слайды
Аннотация. В докладе дается обзор системы Coq — средства для полуавтоматического построения и автоматической проверки доказательств на компьютере. Возможность формальной проверки доказательств теорем особенна ценна в случаях, когда сложность и объём текста доказательства делает его необозримым для человека. Один из известных примеров (о котором пойдёт речь в докладе) — решение задачи о четырёх красках. Ещё одним (возможно, даже более важным) применением Coq является разработка программных продуктов, корректность работы которых доказана формально и которые предназначены для использования в критических ситуациях (например, управление опасными производствами). Одной из важных специфических черт Coq является возможность извлечения реализации алгоритма в виде программы из формального доказательства его корректности.
2020.04.15: Верификация длинных доказательств: мечты, планы и реальность
Докладчик: Шабат Георгий Борисович (РГГУ, МПГУ, Независимый Московский Университет)
Видеозапись доклада: YouTube | слайды
Аннотация. Речь в основном пойдет о незавершенном проекте Владимира Воеводского (предварительный итог которого подведен в коллективной монографии [1]), в котором предполагалось существенно расширить взаимодействие математиков c компьютерами при построении и проверке доказательств.
После краткого обзора унивалентных оснований математики внимание будет сосредоточено на проблемах, возникающих в связи с доказательствами, традиционное понимание которых затруднено или невозможно по причине их длины и сложности. Будут приведены примеры; позиции докладчика будут критически сопоставлены с положениями известного провокационного текста Николая Вавилова [2].

В заключение будут высказаны соображения о формализации преподаваемой математики.
[1] Homotopy Type Theory: Univalent Foundations for Mathematics. Univalent Foundations Project, Institute for Advanced Study, 2013. (465 pages) arXiv: 1308.0729
[2] Nikolai Vavilov. Reshaping the metaphor of proof. Philosophical Transactions of the Royal Society A. Mathematical, Physical, and Engineering Sciences, 2019. DOI: 10.1098/rsta.2018.0279
2020.03.11: Гипотеза чувствительности и ее доказательство
Докладчик: Подольский Владимир Владимирович, ФКН ВШЭ, МИАН.
Видеозапись доклада: YouTube
Аннотация. Чувствительностью булевой функции f на входном наборе x называется количество таких переменных, что изменение значения x в этой переменной меняет значение функции. Чувствительностью булевой функции f называется максимум ее чувствительности по всем входным наборам x. Аналогично можно определить понятие блочной чувствительности, в котором вместо изменения одной переменной можно менять значение целого блока переменных.
Гипотеза чувствительности утверждает, что эти две величины полиномально связаны, то есть каждая из них выражается как полином от другой. Эта гипотеза оставалась открытой с 1992 года и была доказана летом 2019 года в работе Хао Хуанг [1]. Доказательство при этом оказалось совсем несложным. В докладе мы расскажем об этой гипотезе и о связях ее с другими вопросами в теории сложности вычислений. Если позволит время, будет также рассказана идея доказательства.
[1] Hao Huang. Induced subgraphs of hypercubes and a proof of the Sensitivity Conjecture. July 2019, arXiv.
2020.02.26: Алгебры Клини с делениями и их теории
Докладчик: Кузнецов Степан Львович
Видеозапись доклада: YouTube
Аннотация. Операции делений в частично упорядоченных алгебраических структурах восходят ещё к довоенным работам Крулля, Варда и Дилворта. Структуры, в которых вместе с делениями присутствует операция итерации («звёздочка Клини»), называются алгебрами Клини с делениями. Вопрос об алгоритмической разрешимости эквациональной теории (т.е. множества общезначимых равенств термов) для класса всех алгебр Клини с делениями поставил Козен в 1994 г. Ответ на вопрос отрицателен; будет изложена схема доказательства неразрешимости. Помимо этого, будет дан обзор смежных результатов о сложности теорий классов алгебр Клини с делениями.
[1] S. Kuznetsov. The logic of action lattices is undecidable. LICS 2019, IEEE, 2019, 9 pp. (pdf)
[2] S. Kuznetsov. Action logic is undecidable. 2019, arXiv:1912.11273
[3] S. Kuznetsov. *-continuity vs. induction: divide and conquer. AiML vol. 12, College Publications, 2018, pp. 439-510. (pdf)
[4] S. Kuznetsov. The Lambek calculus with iteration: two variants. WoLLIC 2017, LNCS vol. 10388, Springer, 2017, pp. 182-198. (arXiv:1705.07309)

ОСЕНЬ 2019

2019.12.18: Об изоморфизме Концевича и его независимости от выбора бесконечно большого простого числа
Докладчик: Елишев Андрей Михайлович, кафедра дискретной математики МФТИ.
Соавтор: Канель-Белов Алексей Яковлевич.
Видеозапись доклада: YouTube 
Аннотация. Гипотеза Концевича (2005) утверждает существование изоморфизма между группой автоморфизмов алгебры Вейля W_n и группой полиномиальных симплектоморфизмов аффинного пространства размерности 2n над полем характеристики нуль.
Доклад посвящен доказательству этой гипотезы, предложенному недавно авторами совместно с Дж.-Т. Ю в статьях [1] и [2]. Конструкции в доказательстве используют приложения теории моделей, в частности, элементы нестандартного анализа. 
В докладе будут сформулированы необходимые определения из алгебры и элементов теории моделей. Далее будет проведено построение гомоморфизма Φ: Aut W_n,ℂ → Aut P_n,ℂ (биективность которого устанавливается в [1]), основанное на процедуре редукции по модулю бесконечно большого простого числа, а также рассмотрен вопрос о независимости этого построения от выбора ультрафильтра на множестве индексов и бесконечно большого простого [2]. Также предполагается обсудить связь гипотезы Концевича с проблемой якобиана.
[1] Alexei Kanel-Belov, Andrey Elishev, Jie-Tai Yu. Augmented polynomial symplectomorphisms and quantization, 2018, arXiv
[2] Alexei Kanel-Belov, Andrey Elishev, Jie-Tai Yu. Independence of the B-KK isomorphism of infinite prime, 2019, arXiv
2019.12.04: У структуры (ℕ,<) нет максимального разрешимого обогащения
Докладчики: Семенов Алексей Львович, Сопрунов Сергей Федорович
Видеозапись доклада: YouTube | слайды
Аннотация. В 1966 году Рабин и Элгот [1] поставили проблему существования счетной структуры с конечной сигнатурой, теория которой разрешима, но любое нетривиальное обогащение структуры новым отношением дает неразрешимую теорию.
Для случая слабой монадической теории эта проблема была решена С. Ф. Сопруновым в 1988 году [2]. Для элементарного и монадического случая полного решения проблемы неизвестно.
В докладе будет изложено принадлежащее С. Ф. Сопрунову решение проблемы для случая элементарных теорий произвольных структур, обогащающих порядок на натуральных числах [3,4]. Будет доказано, что у всякой разрешимой (то есть имеющей разрешимую теорию) структуры (ℕ,Σ), где конечная сигнатура Σ содержит предикат < (или в которой он выразим), существует обогащение (одноместным предикатом, не выразимым в сигнатуре Σ), также являющееся разрешимым.
[1] Elgot C., Rabin M. Decidability and undecidability of extensions of second (first) order theory of (generalized) successor. Journal of Symbolic Logic, 1966, vol. 31, no. 2, pp. 169–181.
[2] Сопрунов С.Ф. Разрешимые обогащения структур. Вопросы кибернетики, 1988, вып. 134, с. 175–179.
[3] Soprunov S. An infinite branch in a decidable tree. 22 Mar 2018. arXiv:1801.00423.
[4] Soprunov S. There is no maximal decidable expansion of the (ℕ,{<}) structure. 20 Nov 2019. arXiv:1911.09059.
2019.11.13: Шум увеличивает сложность: вероятностный, комбинаторный и алгоритмический подходы
Докладчик: Александр Шень
Соавтор: Глеб Пособин
Видеозапись доклада: YouTube | слайды
Аннотация. Доклад по работе: Random noise increases Kolmogorov complexity and Hausdorff dimension.
Начиная с работ Колмогорова, можно проследить возможность перевода математических утверждений между тремя «языками» — вероятностным, комбинаторным и сложностным. В докладе предполагается краткий обзор основных результатов в этом направлении, а также более подробный разбор недавнего результата: применение «шума» (каждый бит слова с небольшой вероятностью меняется) увеличивает энтропию/сложность/размер — это неформальное утверждение будет сформулировано на этих трёх языках и объяснено, как переход от одного языка к другому позволяет получить его доказательство.
2019.10.23: Комбинаторика замощений (“многомерных слов”). Применения в алгебре
Докладчик: Иванов-Погодаев Илья Анатольевич, кафедра дискретной математики МФТИ.
Соавтор: Канель-Белов Алексей Яковлевич.
Видеозапись доклада: YouTube | слайды
Аннотация. Множество классических результатов в алгебре и логике опирается на анализ слов и их соотношений. Но есть ситуации, когда удобно применить двумерные аналоги слов — мозаики и замощения. Используя конечный набор плиток, дающий лишь непериодические замощения, можно строить конечноопределенные объекты: полугруппы и группы. Свойства полученных объектов возникают из свойств соответствующих замощений. Такой подход, в частности, позволяет построить конечноопределенную бесконечную нильполугруппу (решение проблемы Шеврина — аналог Теоремы Новикова – Адяна).
Этот же метод позволяет построить негиперболическую группу с неположительной кривизной, не содержащую ℤ×ℤ в качестве подгруппы.
2019.10.09: Вычислимая теория моделей и примитивная рекурсивность
Докладчик: Калимуллин Искандер Шагитович, Казанский (Приволжский) федеральный университет.
Видеозапись доклада: YouTube | слайды
Аннотация. Доклад посвящен исследованиям примитивной рекурсивности на алгебраических структурах в контексте проблем общей теории вычислимых моделей. Полученные совместно с российскими и зарубежными соавторами результаты докладчика демонстрируют ряд неожиданных связей примитивной рекурсии с вопросами чистой теории моделей, а также с общими алгоритмическими вопросами на структурах.
Так, вопрос о существовании примитивно рекурсивных копий алгебраических структур оказывается связанным с понятиями копируемых и диагонализируемых классов структур, введенными А. Монталбаном (2013). Проблема описания структур, имеющих примитивно рекурсивные (автоматные) копии, в некотором смысле оказывается эквивалентной проблеме описания 0'-вычислимых структур, имеющих вычислимые копии.
С другой стороны, вопросы примитивно рекурсивной сложности алгебраических структур и отношений на них оказывается связанным со значениями беcкванторных формул, в параметры которых подставляются попарно различные элементы структуры. Кроме того, структуры, между копиями которых изоморфизм находится равномерно примитивно рекурсивно, образует специальный класс счетно-категоричных структур, имеющий чисто теоретико-модельное описание.

ВЕСНА 2019

2019.05.29: Сравнение коммуникационной, информационной и вопросной сложности
Докладчик: Козачинский Александр Николаевич, асп. 4-го года, науч. рук. Н.К.Верещагин 
Аудитория: 16-16.
Аннотация. Все виды сложности, о которых пойдет речь в докладе, — коммуникационная, информационная и вопросная — в простейшем варианте измеряют сложность булевых функций. Задача состоит в преобразовании входа для функции f в значение f на нем. В обычной алгоритмической сложности вход дается нам целиком, и чем быстрее можно найти значение f, тем функция проще.
Коммуникационная сложность отличается от этого тем, что вход разрезается на две части и делится между двумя игроками, Алисой и Бобом. Их задача та же — вычислить значение f. За единицу времени им разрешается послать один бит от одного игрока к другому. Считая, что любые локальные вычисления бесплатны (не занимают совсем никакого времени), насколько быстро мы теперь можем вычислить f? Эта величина и называется коммуникационной сложностью функции f.
В вопросной сложности вход снова дается нам целиком. При этом бесплатны любые операции, кроме чтения битов входа (чтение одного бита занимает единицу времени).
Наконец, информационная сложность определяется также, как и коммуникационная, за исключением того, что посылка одного бита может занимать меньше единицы времени. Например, случайный бит, независимый от входов игроков, может быть послан бесплатно. В общем случае время на посылку бита пропорционально количеству информации, которое содержится в этом бите о входе посылающего (строго это количество информации определяется при помощи энтропии Шеннона).
Теоремы, связывающие коммуникационную и вопросную сложность, оказываются полезны в схемной сложности. Рассмотрение информационной сложности позволяет отвечать на некоторые вопросы в коммуникационной сложности. Будет рассказано о результатах докладчика на эти темы.
2017.04.24: Научная конференция «Ломоносовские чтения 2019»
Видеозапись: YouTube
Доклады:
1. Об одном информационном неравенстве и его комбинаторном применении.
  Докладчик: проф. Н. К. Верещагин.
2. Критерии аксиоматизируемости в модальной логике.
  Докладчик: с.н.с. Е. Е. Золин.
3. Программа Гильберта, теорема о полноте, теорема о неполноте для математика.
  Докладчик: акад. РАН А. Л. Семёнов.
4. О фрагментах модальных логик предикатов с одной переменной.
  Докладчик: проф. В. Б. Шехтман.
2019.04.11: Логика Гейтинга — Оккама и гиперинтенсиональность
Докладчик: Одинцов Сергей Павлович (Новосибирский государственный университет)
Доклад состоялся в четверг в 18:30 в ауд. 13-04 на совместном заседании НИС и «Модальная и алгебраическая логика».
Аннотация. Поводом для доклада послужило выступление Ханнеса Ляйтгеба на LP18, где он ввел логику HYPE для рассуждений о гиперинтенсиональных контекстах. Оказалось, что эта логика близка к логике Гейтинга — Оккама, введенной в процессе исследования логических программ с отрицанием, т.е. с совершенно иной мотивацией. К тому же обе логики имеют примечательную характеризацию в рамках теории отрицания Вакарелова. Наконец, после представления упрощенной семантики Крипке и алгебраической семантики для HYPE станет ясно, что это типичный пример интенсиональной логики. В значительной степени это будет исторический доклад, включающий краткие обзоры теории отрицания Вакарелова и сведений о дедуктивных базах для немонотонных логик.
2019.04.10: Конференция студентов, аспирантов и молодых учёных «Ломоносов 2019»
Видеозапись: YouTube
Доклады:
1. Ищенко Дарья Дмитриевна
  (МГУ, 3-й курс, научый руководитель: с.н.с. Е. Е. Золин)
  Бисимуляции для градуированного модального языка)
2. Коновалов Александр Юрьевич
  (МГУ, к.ф.-м.н., научный руководитель: доц. В. Е. Плиско)
  Понятие общерекурсивной реализуемости
3. Никитин Игорь Александрович
  (МГУ, 6-й курс, научный руководитель: проф. Н. К. Верещагин)
  Сравнение коммуникационных протоколов (для предикатов)
4. Оноприенко Анастасия Александровна
  (МГУ, асп. 1 года, научный руководитель: чл.-корр. РАН Л. Д. Беклемишев)
  Пропозициональная логика задач и высказываний
5. Пшеницын Тихон Григорьевич
  (МГУ, 2 курс)
  Групповые грамматики и контекстно-свободные грамматики
6. Царегородцев Кирилл Денисович
  (МГУ, асп. 2 года каф. высшей алгебры, научный руководитель: доц. А. Е. Панкратьев)
  О взаимно-однозначном соответствии между правильными семействами булевых функций и реберными ориентациями с единственным стоком на булевых кубах
2019.03.20: Апериодические траектории для внешних биллиардов и компьютер в доказательствах
Докладчик: Рухович Филипп Дмитриевич, кафедра дискретной математики МФТИ.
Соавтор: Канель-Белов Алексей Яковлевич.
Видеозапись доклада: YouTube
Аннотация. Рассмотрим многоугольник G. Из точки A на плоскости проведем (правую) касательную к G. Она пройдет через вершину M многоугольника, отразим точку A относительно этой вершины. Полученное преобразование точек называется преобразованием внешнего биллиарда. При последовательном применении преобразования траектория точки может оказаться периодической, апериодической, а также вырожденной (попадет на сторону многоугольника).
Ситуация проста для 3-, 4- и 6-угольника (все невырожденные траектории периодичны), исследована для 5- и 10-угольника. Автор получил результаты для 8- и 12-угольника.
В докладе пойдет речь о том, как устроены периодические, апериодические и вырожденные точки, периоды и периодические слова точек, как соответствующие множества точек расположены на плоскости, и почему компьютер оказался практически необходимым для полноценного исследования.
2019.03.06: Unsound rules and proof macros
Докладчик: Matthias Baaz (Vienna University of Technology)
Видеозапись доклада: YouTube
Abstract. We give examples of analytic sequent calculi LK+ and LK++ that extend Gentzen's sequent calculus LK by unsound quantifier rules in such a way that
(i) derivations lead only to true sequents;
(ii) cut free proofs may be non-elementary shorter than cut free LK proofs.
This research is based on properties of Hilbert's epsilon calculus and is part of efforts to complement Hilber's stepwise concept of proof by useful global concepts. We use these ideas to provide analytic calculi for Henkin quantifiers and demonstrate soundness, (cut free) completeness and cut elimination. Furthermore, we show that, in the case of quantifier macros such as Henkin quantifiers for a partial semantics, global calculi are the only option to preserve analyticity.
2019.02.20: Исследование вычислительной сложности задач о независимом множестве и о вершинной k-раскраске в некоторых классах графов
Докладчик: Сироткин Дмитрий Валерьевич (НИУ ВШЭ, Нижний Новгород)
Видеозапись доклада: YouTube | слайды
Аннотация. Хорошо известно, что задачи о независимом множестве (НМ) и вершинной раскраске в три цвета (Раскраска) NP-полны в классе всех графов. В докладе рассматриваются вопросы о том, что произойдет, если тем или иным способом сузить класс графов: для каких классов графов задачи НМ и Раскраска остаются NP-полными, а для каких становятся разрешимыми за полиномиальное время. Для этого определяются некоторые локальные преобразования на графах, сохраняющие наличие независимого множества или 3-раскраски. При помощи данных преобразований, а также новых приемов алгоритмической теории графов, получены ответы на эти вопросы для некоторых подклассов класса планарных графов, определяемых запрещенными порожденными структурами малого размера.

ОСЕНЬ 2018

2018.12.19: Заседание, посвященное памяти проф. В. А. Успенского
Видеозапись: YouTube
Доступны также фотографии (за них благодарим Ксению Семёнову)
С докладами выступили:
&bullet; к.ф.-м.н. Александр Шень и
&bullet; проф. Владимир Александрович Плунгян
с обзором, соответственно, математического и нематематического научного наследия заведующего (с 1993 по 2018 гг.) кафедрой математической логики и теории алгоритмов профессора В. А. Успенского (27.11.1930–27.06.2018).
Своими воспоминаниями о В. А. Успенском также поделились (ссылки на соответствующие моменты видеозаписи):
&bullet; акад. Сергей Иванович Адян
(включая комментарий к зачитанному
А. Л. Семеновым поздравлению
с 60-летием проф. Н. К. Верещагина,
ученика В. А. Успенкого),
&bullet; акад. Алексей Львович Семёнов,
&bullet; проф. Владимир Михайлович Тихомиров,
&bullet; проф. Елена Наумовна Зарецкая,
&bullet; проф. Екатерина Владимировна Рахилина.
2018.12.05: Алгоритмическая выразительность неклассических предикатных логик, задаваемых классами шкал Крипке, не определимыми в логике первого порядка
Докладчик: Рыбаков Михаил Николаевич (Тверской государственный университет)
Видеозапись доклада: YouTube | слайды
Аннотация. Известно, что для всякого класса шкал Крипке, определимого в языке первого порядка, соответствующий ему класс предикатных модальных логик рекурсивно аксиоматизируем. То же верно для предикатных суперинтуиционистских логик. В то же время известно, что добавление существенно второпорядковых условий (в различных их формах) к семантике во многих случаях приводит к потере рекурсивной перечислимости получающейся логики.
В докладе будут приведены примеры существенно второпорядковых условий, которые позволяют получить:
(а) бесконечные классы предикатных модальных (и суперинтуиционистских) неперечислимых логик и неполных по Крипке исчислений;
(б) примеры полных по Крипке рекурсивно аксиоматизируемых предикатных модальных логик, которые не полны относительно первопорядково определимых классов шкал (и/или классов порождённых корневых шкал).
Если останется время, то будут представлены результаты, связанные с неразрешиостью и неперечислимостью модальных и суперинтуиционистских предикатных логик в языке с одной одноместной предикатной буквой и малым числом (2-3) предметных переменных.
2018.11.21: Секвенциальные исчисления с нефундированными выводами для логик Гжегорчика
Докладчик: Саватеев Юрий Вячеславович.
Соавтор: Шамканов Данияр Салкарбекович.
Видеозапись доклада: YouTube
Аннотация. В докладе будут предложены секвенциальные исчисления с нефундированными выводами для логики Гжегорчика Grz и слабой логики Гжегорчика wGrz. Для этих исчислений строится оператор удаления сечения как неподвижная точка нерастягивающего отображения в ультраметрическом пространстве.
2018.11.07: Сложность конечных автоматов в терминах количества состояний и ее поведение при различных операциях
Докладчик: Раскин Михаил Александрович
Видеозапись доклада: YouTube | слайды
Аннотация. Детерминированные и недетерминированные конечные автоматы распознают одно и то же семейство языков. Хорошо известно, что детерминизация может приводить к экспоненциальному росту числа состояний. (Естественно напрашиваются аналогии с проблемой перебора.) Можно выделить некоторые промежуточные классы конечных автоматов, например, однозначные конечные автоматы, а также различные другие модификации конечных автоматов. Операции над языками при разных представлениях будут по-разному влиять на количество состояний.
В докладе будет дан обзор результатов о сложности в терминах количества состояний для разных видов автоматов и приведены некоторые новые результаты.
2018.10.24: Computability aspects in multidimensional symbolic dynamics (на английском языке)
(Алгоритмические свойства многомерных замощений)
Докладчик: Pierre Guillon (Пьер Гийон) (CNRS & Centre interdisciplinaire franco-russe Poncelet)
Видеозапись доклада: YouTube | slides
Abstract. A 1D subshift of finite type (SFT) is a set of biinfinite words over a given finite alphabet, defined by prohibiting a finite set of finite patterns. 1D SFT can be studied thanks to linear algebra, graph theory, automata theory. The 2D version of this object, however, corresponds to tilings by Wang tiles, and relies strongly on computability theory.
We will survey some uncomputability and characterization results in this setting: domino problem, language, entropies, traces, periods, quasiperiods, Kolmogorov complexity, Turing degrees. If time permits, we will conclude with open questions, especially in the larger setting of Cayley graphs.
2018.10.10: Экспандеры и связь коммуникационной и вопросной сложности
Докладчики: Козачинский Александр Николаевич и Верещагин Николай Константинович
Видеозапись доклада: YouTube | слайды
Аннотация. Доклад посвящён техникам получения нижних оценок для трёх видов сложности вычислений: схемной (рассматривавшейся начиная с 1950-х годов), коммуникационной и вопросной. Будет описана техника сведения одних оценок к другим и приведены результаты автора, относящиеся к ограниченности этой техники.

Избранные доклады прошлых лет

2018.04.11: Конференция студентов, аспирантов и молодых учёных «Ломоносов 2018»
Доклады:
1. Запрягаев Александр Александрович
  (МГУ, 6 курс, научный руководитель: чл.-корр. РАН Л.Д.Беклемишев)
  Необходимые и достаточные условия интерпретируемости линейных порядков в арифметике Пресбургера
2. Колмаков Евгений Александрович
  (МГУ, аспирант 1 года, научный руководитель: чл.-корр. РАН Л.Д.Беклемишев)
  Аксиоматизация доказуемой 1-доказуемости
3. Торопкин Артем Владимирович
  (МГУ, аспирант 1 года, научный руководитель: доц. Т. Л. Яворская)
  О явном представлении бимодальных логик
2018.04.04: Замощения Аммана
Докладчик: Верещагин Николай Константинович
Аннотация. Доклад по статье Верещагина, Дюрана и Шеня: On the structure of Ammann A2 tilings.
2017.11.22: Конструктивные семантики логических языков, основанные на обобщённой вычислимости
Докладчик: Коновалов Александр Юрьевич
Аннотация. Краткое изложение результатов представляемой к защите диссертации.
Научный руководитель: доц. В.Е.Плиско.
2017.11.15: Interpolation, Amalgamation and Combination (на английском языке)
Докладчик: Silvio Ghilardi (Сильвио Гиларди)
2017.05.31: О некоторых вопросах алгоритмической статистики
Докладчик: Милованов Алексей Сергеевич
Аннотация. Краткое изложение результатов представляемой к защите диссертации.
Научный руководитель: проф. Н.К.Верещагин.
2017.04.19: Научная конференция «Ломоносовские чтения 2017»
Доклады:
1. Нестохастические объекты в алгоритмической статистике.
  Докладчики: Верещагин Николай Константинович (проф.), Милованов Алексей Сергеевич (асп.).
2. О спектрах консервативности для арифметических теорий.
  Докладчик: Беклемишев Лев Дмитриевич (проф., чл.-корр. РАН).
3. О моделировании знания в социальных сетях.
  Докладчик: Крупский Владимир Николаевич (доц.).
4. Кратчайшая перестройка данных графов, одного в другой:
  линейный алгоритм или сведение к целочисленному линейному программированию.
  Докладчик: Любецкий Василий Александрович (проф.).
5. О конструктивной теории перечислимых видов.
  Докладчик: Плиско Валерий Егорович (доц.).
6. О понятии исчисления.
  Докладчики: Семёнов Алексей Львович (проф., академик РАН), Успенский Владимир Андреевич (проф.).
7. О пространствах выразимости.
  Докладчик: Семёнов Алексей Львович (проф., академик РАН).
8. Структура пространств выразимости для следования на целых числах.
  Докладчик: Семёнов Алексей Львович (проф., академик РАН), Сопрунов Сергей Федорович (с.н.с. ВЦ РАН).
9. О полноте некоторых предикатных модальных логик.
  Докладчик: Шехтман Валентин Борисович (проф.).
2017.04.12: Конференция студентов, аспирантов и молодых учёных «Ломоносов 2017»
Доклады:
1. Власов Илья Игоревич
  (Казанский (Приволжский) государственный университет)
  Умеренно низкие и супернизкие множества (аннотация)
2. Запрягаев Александр Александрович
  (МГУ, 5-й курс, научный руководитель: чл.-корр. РАН Л. Д. Беклемишев)
  Интерпретации арифметики Пресбургера в себя
2017.02.15: Об элиминации итеративных операторов в некоторых теориях первого порядка
Докладчик: Золотов Александр Сергеевич (Казанский федеральный университет)
Аннотация. Доклад посвящен исследованию алгоритмических свойств разрешимых арифметических теорий первого порядка, обогащенных итеративными операторами: оператором транзитивного замыкания и оператором фиксированной точки. В некоторых случаях удается эффективно элиминировать данные операторы, что позволяет сделать выводы о разрешимости обогащений. В других случаях обогащение оказывается неразрешимым. Также для фрагмента теории целых чисел с функцией следования и одноместным оператором наименьшей фиксированной точки, применяемым только к экзистенциальным формулам, установлена полнота проблемы разрешимости в классе гиперэкспоненциальной временной сложности.
2016.11.02: Сравнение игровыми методами понятий префиксной и обычной колмогоровской сложности
Докладчик: Андреев Михаил Александрович
Аннотация. Краткое изложение результатов представляемой к защите диссертации.
Научный руководитель: проф. Н.К.Верещагин.
2016.04.27: Научная конференция «Ломоносовские чтения 2016»
Доклады:
1. Бисимуляционные игры и неклассические логики
  Докладчик: Шехтман Валентин Борисович (профессор, д.ф.-м.н.)
2. Модальные логики операций на шкалах Крипке
  Докладчик: Золин Евгений Евгеньевич (с.н.с., к.ф.-м.н.)
2016.04.13: Конференция студентов, аспирантов и молодых учёных «Ломоносов 2016»
Доклады:
1. Вахрушева Полина Викторовна
  (МГУ, аспирант, научный руководитель: проф. В. Б. Шехтман)
  Свойства некоторых временных гибридных логик
2. Запрягаев Александр Александрович
  (МГУ, 4-й курс, научный руководитель: чл.-корр. РАН Л. Д. Беклемишев)
  Интерпретации арифметики Пресбургера в себя
3. Маслов Николай Александрович
  (научный руководитель: проф. В. Б. Шехтман)
  Бисимуляционная игра Эренфойхта для предикатных моделей Крипке с постоянной областью
4. Милованов Алексей Сергеевич
  (МГУ, аспирант, научный руководитель: проф. Н. К. Верещагин)
  Некоторые свойства антистохастических слов
2015.04.15: Конференция студентов, аспирантов и молодых учёных «Ломоносов 2015»
Доклады:
1. Осипов Илья Игоревич
  Теоремы о характеризации для бимодальной логики
2014.05.21: Некоторые результаты об автоматах на сверхсловах, полученные с помощью прямого и полупрямого произведения
Докладчик: Раскин Михаил Александрович
2014.04.16: Научная конференция «Ломоносовские чтения 2014»
Доклады:
1. Коммуникационная сложность приближённого нахождения колмогоровской сложности
  Докладчик: Верещагин Николай Константинович (профессор, д.ф.-м.н.)
2. Локальный аналог теоремы Гольдблатта-Томасона в модальной логике
  Докладчик: Золин Евгений Евгеньевич (с.н.с., к.ф.-м.н.)
2013.09.18: Отношение совместимости в двух вариантах исчисления Ламбека
Докладчик: Сорокин Алексей Андреевич
Аннотация. Краткое изложение результатов представляемой к защите диссертации.
Научный руководитель: проф. М.Р.Пентус.
2013.05.22: Применения графов в теории колмогоровской сложности
Докладчик: Мусатов Даниил Владимирович
Аннотация. Краткое изложение результатов представляемой к защите диссертации.
Научный руководитель: проф. Н.К.Верещагин.
2013.04.24: Научная конференция «Ломоносовские чтения 2013»
Доклады:
1. Вычисление небольшого списка, содержащего короткое описание данного объекта
  Докладчик: Верещагин Николай Константинович (профессор, д.ф.-м.н.)
2. Клетчатые произведения модальных логик
  Докладчики: Шехтман Валентин Борисович (профессор, д.ф.-м.н.), Шапировский Илья Борисович (с.н.с. ИППИ РАН, к.ф.-м.н.)
2013.04.10: Конференция студентов, аспирантов и молодых учёных «Ломоносов 2013»
Доклады:
1. Андреев Михаил Александрович
  (МГУ, 5-й курс, научные руководители: проф. Н. К. Верещагин, А. Шень)
  Различные варианты α-нулевых множеств и их сравнение
2. Колесниченко Игнатий Игоревич
  (МГУ, аспирант, научные руководители: асс. М. А. Бабенко, проф. Н. К. Верещагин)
  О минимальных окончаниях подслов
2012.12.05: Конструкция Хрушовского и гипотезы Шануэля и Андрэ
Докладчик: Зильбер Борис Иосифович
Аннотация. Конструкция Хрушовского является (eдинственным) источником контрпримеров к гипотезе докладчика о том, что все теории, категоричные в несчётных мощностях, сводятся к алгебраической геометрии. Тем не менее, более глубокий анализ показывает, что эти контрпримеры не очень далеки от алгебраической геометрии и связаны с классическими трансцендентными функциями. При этом один из ключевых элементов конструкции Хрушовского соответствует условию, сформулированному в частном случае в известной гипотезе Шануэля, и её глубокому обобщению — гипотезе Ива Андрэ.
2012.10.31:
1) Разрешимость теории иерархий согласованных со сложением функций
Докладчик: Снятков Алексей Сергеевич (Тверской государственный университет)
Аннотация. Краткое изложение результатов представляемой к защите диссертации.
Научный руководитель: д.ф.-м.н., доц. С.М.Дудаков.

2) Эффективные алгоритмы для некоторых задач обработки слов
Докладчик: Стариковская Татьяна Андреевна
Аннотация. Краткое изложение результатов представляемой к защите диссертации.
Научный руководитель: к.ф.-м.н. М.А.Бабенко.
2012.04.11: Конференция студентов, аспирантов и молодых учёных «Ломоносов 2012»
Доклады:
1. Андреев Михаил Александрович (МГУ, 4-й курс)
  Эффективная хаусдорфова размерность и случайность по классам мер
2. Пахомов Федор Николаевич (МГУ, 5-й курс)
  PSpace-полнота замкнутого фрагмента полимодальной логики доказуемости
3. Савин Арсений Анатольевич (МГУ, 4-й курс)
  Тотально вычислимая колмогоровская сложность
2012.03.28:
1) О пропозициональных исчислениях, представляющих понятие доказуемости
Докладчик: Дашков Евгений Владимирович
Аннотация. Краткое изложение результатов представляемой к защите диссертации.
Научный руководитель: проф. Л.Д.Беклемишев.
2) Категориальные грамматики, основанные на вариантах исчисления Ламбека
Докладчик: Кузнецов Степан Львович
Аннотация. Краткое изложение результатов представляемой к защите диссертации.
Научный руководитель: проф. М.Р.Пентус.
2011.12.14: Добавление случайных аксиом и теорема Гёделя
Докладчик: Шень Александр
Аннотация. Теорема Гёделя в форме Чейтина показывает, что утверждения вида «колмогоровская сложность x больше c», где x — конкретное слово, а c — конкретное число, недоказуемы для всех достаточно больших с. С другой стороны, мы практически уверены, что бросание честной монеты позволяет получить пары (x, c), для которых такие утверждения истинны (считая противное невероятным). Что будет, если добавлять такие утверждения в качестве аксиом? Можно ли таким образом преодолеть ограничения, накладываемые теоремой Гёделя? В докладе этот вопрос будет уточнён и показано (в некотором точном смысле), что надежды получить новые интересные утверждения таким способом нет, а вот сокращение доказательств тут возможно.
2011.11.16: Научная конференция «Ломоносовские чтения 2011»
Доклады:
1. Проблема глобальной выполнимости в полимодальных градуированных логиках
  Докладчик: Золин Евгений Евгеньевич (с.н.с., к.ф.-м.н.)
2. Квадраты модальных логик с дополнительными связками
  Докладчик: Шехтман Валентин Борисович (профессор, д.ф.-м.н.)
3. Интерполяционные свойства логик доказуемости и нормализация термов рефлексивной комбинаторной логики
  Докладчик: Шамканов Данияр Салкарбекович (аспирант)
  Аннотация. Краткое изложение результатов представляемой к защите диссертации.
  Научные руководители: проф. Л.Д.Беклемишев, доц. В.Н.Крупский.
2010.09.22: О некоторых суперинтуиционистских логиках, связанных с логикой задач Колмогорова – Медведева
Докладчик: Шатров Тимофей Анатольевич
Научный руководитель: проф. В.Б.Шехтман

Научно-исследовательский семинар по математической логике

руководители: академик РАНакадемик РАН Лев Дмитриевич Беклемишев Алексей Львович Семёнов

руководители:

академик РАН
академик РАН Лев Дмитриевич Беклемишев
Алексей Львович Семёнов