Кафедра математической логики и теории алгоритмов мехмата МГУ
298 subscribers
44 photos
336 links
Учёный секретарь кафедры @ansidiana
Download Telegram
#матлог #учёба #спецсеминар #отмены

16.10.2025 заседания семинара «Вероятностные и субструктурные логические системы» (https://www.mathnet.ru/conf2533) не будет.
Следующее заседание — 23.10.2025.

ВК
#матлог #учёба #спецсеминар

Семинар "Вычислимость и неклассические логики" работает по пятницам с 16.45 в аудитории 425.

17 октября 2025 г.

А. В. Тюленев
“Вычислимость решений начальной задачи для дифференциальных уравнений с отклоняющимся аргументом нейтрального типа”

Аннотация - в приложенном файле.

📝 Аннотация_выч_реш_НУ.pdf

ВК
#матлог #учёба #спецсеминар #не_мехмат #МИАН #ТД

Logic Online Seminar (www.mathnet.ru/conf876), Monday 16:00 MSK (UTC+3), Kontur Talk (online only)

20.10.2025 Д. Рогозин (Noeon Research, Великобритания). «Категорные модели линейной теории типов с субэкпоненциальными модальностями» - продолжение доклада от 13 октября 2025 года.

Субэкспоненциалы являются естественным обобщением экспоненциального оператора из линейной логики. Если экспоненциал ограниченно вводит правила сокращения и ослабления, тогда как субэкспоненциал, в общем случае, — это модальный оператор, чьи формальные свойства напоминают оператор $\Box$ в логике S4, который либо вводит правило ослабления (аффинный субэкспоненциал), либо правило сокращения (релевантный субэкспоненциал), либо оба, либо ни одного. В литературе ранее изучались полимодальные обобщения линейной логики с субэкспоненциалами в контексте теории доказательств и конкретных применений в прикладной информатике, но семантический анализ был проведен довольно ограниченно. В этом докладе, мы введем теоретико-типовую версию интуиционисткой линейной логики с субэкспоненциалами и кратко обсудим её теоретико-доказательные аспекты, в частности, нормализацию выводов. Далее мы введем ряд понятий, позволяющих ввести адекватную денотационную семантику, основанную на симметрических моноидальных замкнутых категорий, снабженных семейством комонад определенного рода и естественных преобразований между ними. Далее, мы дадим обобщение ряда результатов из 1990-х годов и покажем, как модели таких систем типов эквивалентно характеризуются как так называемые моноидальные сопряжения. В частности, мы покажем как осуществить такую характеризацию 2-категории всех моделей как полной 1,2-подкатегории 2-категории 2-функторов определенного вида. По возможности, автор постарается дать пропедевтическое введение в необходимые понятия и факты из теории 2-категорий и формальной теории комонад.

ВК
4
#матлог #учёба #семинар #не_мехмат #ВШЭ

Уважаемые коллеги, приглашаем вас принять участие в заседании научного семинара "Современные проблемы математической логики" в ВШЭ.

Семинар пройдет в очном формате с одновременной трансляцией
на Математическом факультете ВШЭ, в аудитории 109 (ул. Усачева, д. 6). Мы будем транслировать доклад в zoom, но лучше приходите очно.
Если вам нужен пропуск в здание матфака, пришлите ваши ФИО и просьбу о пропуске на почту [email protected].

Дата и время: 17.10.2025 в 16:20

Название: Проективность и свойство расширения для логики GL

Докладчик: Никита Лукашов

Аннотация:
В своём докладе я расскажу результаты С. Гилярди о семантической характеризации проективных формул для некоторых модальных логик на примере конкретной модальной логики доказуемости GL. В частности, я постараюсь полностью привести доказательство того, что формула A является проективной в логике GL тогда и только тогда, когда класс MOD(A) конечных GL-моделей Крипке с корнем формулы A обладает некоторым определённым свойством расширения.
Этот результат оказался полезным, во-первых, для решения проблемы унификации в популярных модальных логиках, таких как K4, S4, GL,… — все они имеют конечный тип (Гилярди, 2000 г.); во-вторых, семантическая характеристика проективных формул послужила основой для получения Э. Ержабеком (2005 г.) явного базиса допустимых правил вывода в этих логиках.

Доклад основан на статье: Ghilardi S. Best solving modal equations //Annals of Pure and Applied Logic. – 2000. – Т. 102. – №. 3. – С. 183-198.

ВК
👍1
#матлог #учёба #спецсеминар

Kolmogorov seminar on complexity (for receive the zoom link, please email [email protected])

20 October, 18:30 MSK

In this talk Maxim Ushakov (who has some experience in using AI tools and developing them at a small scale) will share his experiences and answer our questions. Here are the some questions.

Few years ago we heard that LLM are advanced token predictors: the dialog stream is split into tokens and then the "most probable" next token is predicted (not just using good old statistical counting but some more advanced "machine learning" tools). Obviously what we see now goes far beyond that, and something obviously impossible happens. But what is under the hood? More specific questions: - Are there separate stages while preparing the answer? (ChatGPT even produces some reasonably looking names for these stages) What happens during this stages?

- How the engine interacts with other programs like programming language interpreters, formal provers etc.? If I ask it to give an approximate solution of some equation (or just ask to multiply two 10-digit integers), does it run some math software? If I ask you to debug some code, does it tries to run it in the debugger? If I ask it when will be the next concert of Angela Hewitt, does it perform internet search? How all this is organized?

- How the model uses the token-prediction engine (probably several times)?

- What is the entire cycle of developing and using the model? It is trained (as predictor of tokens or as a whole), then fine-tuned, then specialized using a prompt, and then applied to some request? What are the costs and resources needed for each step? What can be done inside a medium company like Yandex, in a small startup company like your friends try to create, locally at good home computer, or in a mobile phone?

- What is preserved during the dialog with AI model and between the dialogs?

- What amount of information needs to be learned to get some new "skill"? For example, can it learn ancient Greek or some other language where we have only a limited amount of texts in the language like people do (studying grammar textbooks, making graded exercises etc.)? Is is possible to learn some new mathematical theory just by reading the only textbook on this theory (and may be having some dialogs with experts)? Is the technology more or less known to all the players (companies — from Yandex to OpenAI) and the difference is just the resources and few years of development, or there are some "key secrets"? Related question: these companies hire key people for millions, presumably those people have some much needed knowledge/abilities. What are those abilities and where they come from? What kind of topics and experiences should be included in the curriculum to prepare to the New World? Linguistics and logic seem to be in big trouble (even if they don't see it now like this): it turns out that the «rigid» structures like grammars and formal theories they tried to discover and develop are not something fundamental but appear from the sea of fuzzy parameters in quite mechanical (though probably not understood) way, and what looked like syntactical sugar and user-friendly interface could be much more fundamental -In general, what are the current frontiers between what is easy / difficult / very difficult and expensive / hardly possible / out of reach? What is now possible locally (on a reasonable desktop) in terms of education/reeducation/dialog
?

- What is happening in specialized topics like audio/video/photo analysis and generation? Can the models write down the score of a symphony looking at the video (with sound), or find an error in the performance of a Beethoven's sonata? How do they do it (what is replacing the tokens etc.)?

If all goes well, we can have some live experiments and comments (a session of magic and its exposure).

ВК
#матлог #учёба #просеминар

💥В среду 22 октября состоится очередное занятие просеминара по математической логике и информатике.

Тема: "Интуиционистская логика (продолжение 2)" (Андрей Ерёмин, студент философского факультета МГУ; Оноприенко А.А.).
Аннотация. В конце XIX — начале XX века в наивной теории множеств был обнаружен ряд противоречий. Это привело к необходимости пересмотра имеющихся оснований математики с целью найти новые: строгие, убедительные и свободные от противоречий.
Один из подходов, называемый интуиционизмом, был предложен математиком Л. Э. Я. Брауэром. Согласно Брауэру, математика есть в первую очередь творческая деятельность, разворачивающаяся в разуме математиков. Поэтому, дабы избежать парадоксов, из рассмотрения следует исключить объекты, которые принципиально невозможно сконструировать в человеческом уме. А это, в свою очередь, ведет к пересмотру ряда логических принципов, влекущих так называемые «теоремы чистого существования», и самого понятия математической истины.
Ученик Брауэра А. Гейтинг формализовал предлагаемые Брауэром модификации классической логики. Полученная формальная система активно изучается; были получены глубокие результаты, связанные с другими областями математической логики.
На просеминаре мы разберем основные сюжеты и определения, связанные с её пропозициональным вариантом: интуиционистской логикой высказываний.
Можно заранее порешать задачи (прикреплены к посту).

Просеминар проходит по средам в 15:00-16:35 в аудитории 406 (2 гуманитарный корпус).
По просьбам участников создан чат просеминара в телеграме: https://t.iss.one/+8lzSUf8ghLAzMjRi
Информацию о просеминаре можно найти на странице logic.math.msu.ru/proseminar/.
К сожалению, сайт кафедры сейчас работает нестабильно, поэтому ориентируйтесь на информацию в группе кафедры ВК или в телеграм-канале по хештегу #просеминар

ВК
1
#матлог #учёба #спецсеминар

Семинар «Вероятностные и субструктурные логические системы» (www.mathnet.ru/conf2533) под руководством С.Л. Кузнецова (homepage.mi-ras.ru/~sk/) и С.О. Сперанского (homepage.mi-ras.ru/~speranski/).

Время: 23 октября (четверг), 16:00
Место: МИАН, ауд. 530 + Контур.Толк

В.А. Нестеров (МФТИ)

Название:
Верифицированное вычисление асимптотик вещественных функций

Аннотация:
Вычисление асимптотик функций - одна из нетривиальных математических задач, которая, однако, под силу компьютеру. Исследования в этом направлении были начаты Г. Харди, и доведены до практического алгоритма Дж. Шекеллом в 1990 году.

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

Если планируете посетить заседание (очно или онлайн через Контур.Толк), пожалуйста, зарегистрируйтесь по ссылке в верхней части страницы семинара:

https://www.mathnet.ru/conf2533

ВК
👍2
#матлог #спецсеминар #не_мехмат #МФТИ

Уважаемые коллеги, приглашаем вас на логический семинар лаборатории им. Манина Высшей школы современной математики МФТИ (ВШМ).
Страница семинара: www.mathnet.ru/rus/conf2559.

Семинар пройдет в среду 22 октября в 14:00.

Место проведения: ОНЛАЙН. Для получения ссылки пишите на почту [email protected].

Можно подключиться самостоятельно, а можно подойти по адресу, МФТИ, Административный корпус, ауд. 322, Первомайская ул. д.7, Долгопрудный.
Чтобы пройти на семинар, если у вас нет пропуска в МФТИ, достаточно сказать, что вы идете на семинар ВШМ и предъявить паспорт.

Докладчики: Д.П. Шкатов (Университет Йоханнесбурга, ЮАР)

Название: Введение в семантику первопорядковых модальных логик

Аннотация.

Будут разъяснены основные понятия семантики Крипке для предикатных модальных логик. Предполагается знакомство слушателей с пропозициональными модальными логиками, хотя основные понятия, касающиеся этих логик, будут кратко напомнены.

ВК
#матлог #спецсеминар #нпммвя

В четверг 23 октября в Математическом институте им. В.А. Стеклова РАН состоится заседание семинара "Некоторые применения математических методов в языкознании" с продолжением доклада "База коннекторов русского языка Рускон: проблемы и задачи представления лексикографических данных".

Время: 23 октября, 14:00-15:30.
Место: Математический институт им. В.А. Стеклова РАН, ул. Губкина, д. 8, ауд. 104. Для прохода потребуется студенческий/пропуск любой образовательной или научной организации либо паспорт.

Ссылка для регистрации: https://forms.gle/SSCTfuuTVwGMs4TS8

Докладчики:
Сердобольская Наталья Вадимовна (ИЯз РАН),
Кобозева Ирина Михайловна (МГУ, ИЯз РАН),
Тимошенко Светлана Петровна (ИППИ РАН, РГГУ)

Тема: «Составные коннекторы в базе Рускон: союзы, коннекторы и свободные сочетания»

Анонс:
Вторая часть доклада посвящена проблемам выделения класса составных коннекторов русского языка в базе Рускон. Академические словари и грамматики серьезно расходятся в мнениях по поводу трактовки конкретных сочетаний – как в плане их лексико-грамматического статуса, так и, шире, в плане включения их в базовый инвентарь. В изданиях используются термины «в значении союза», «аналог союза», «союзное соединение» и т.п. Это связано с трудностью разграничения единых союзов (потому что) и окказиональных сочетаний (а из-за этого) – условно говоря, единиц, которые содержатся в памяти как единое целое или порождаются в ходе речепроизводства.
Мы рассматриваем критерии определения составных коннекторов, которые работают на различных уровнях языка – фонетические, морфологические, синтаксические и семантические критерии. В некоторых случаях эти лингвистически обоснованные критерии не дают однозначного ответа. Был проведен ряд экспериментов, в ходе которых коннекторы ранжировались с помощью различных метрик устойчивости словосочетаний. Наилучшие результаты показали метрики, производные от меры точечной взаимной информации (Pointwise Mutual Information, сокращенно PMI). Мы предлагаем использовать при решении аналогичных задач модификацию MMI (Modified Mutual Information), адаптированную для оценки словосочетаний произвольной длины.

ВК
👍2
#матлог #учёба #семинар #не_мехмат #ВШЭ

Уважаемые коллеги, приглашаем вас принять участие в заседании научного семинара "Современные проблемы математической логики" в ВШЭ.

Семинар пройдет в очном формате с одновременной трансляцией
на Математическом факультете ВШЭ, в аудитории 109 (ул. Усачева, д. 6). Мы будем транслировать доклад в zoom, но лучше приходите очно.
Если вам нужен пропуск в здание матфака, пришлите ваши ФИО и просьбу о пропуске на почту [email protected].

Дата и время: 24.10.2025 в 16:20

Название: Проективность и свойство расширения для логики GL, Часть II

Докладчик: Никита Лукашов

Аннотация:
В первой части доклада мы подробно рассмотрели проблему унификации для логик, обсудили определение типа унификации для них, а также привели полное доказательство того, что классическая пропозициональная логика CL обладает унитарным типом унификации. Для установления последнего результата мы использовали так называемые проективные формулы, определение которых мы привели для произвольных логик и доказали их основные свойства.

Во второй части доклада мы продолжим доказательство семантической характеризации С. Гилярди (2000 г.) проективных формул для модальных логик на примере конкретной модальной логике доказуемости GL. Я коротко напомню про семантический подход к проблеме унификации из первой части, а затем перейду к рассказу доказательства того, что формула A является проективной в логике GL тогда и только тогда, когда класс MOD(A) конечных GL-моделей Крипке с корнем формулы A обладает некоторым определённым свойством расширения.

Если останется время, то я также расскажу, как из полученной семантической характеризации проективных формул доказать конечный тип унификации логики GL (соответственно, рассуждение из второй части статьи ниже).

Доклад основан на статье: Ghilardi S. Best solving modal equations //Annals of Pure and Applied Logic. – 2000. – Т. 102. – №. 3. – С. 183-198.

ВК
#матлог #учёба #спецсеминар

Kolmogorov seminar on complexity (for receive the zoom link, please email [email protected])

27 September, 18:30 MSK
Fedor Kiselyov will discuss randomized and deterministic reductions between problems in TFNP (a more detailed abstract is attached).

📝 Kiselyov.pdf

ВК
#матлог #учёба #спецсеминар #не_мехмат #МИАН #ТД

Logic Online Seminar (www.mathnet.ru/conf876), Monday 16:00 MSK (UTC+3), Kontur Talk (online only)

27.10.2025 А.С. Морозов (ИМ СО РАН, https://www.mathnet.ru/php/person.phtml?option_lang=rus&personid=19694): Представимость алгебраических структур над вещественными числами.

Изучаются два обобщения понятия вычислимой структуры: $\Sigma$-представимости алгебраических структур в наследственно конечной надстройке HF(R) над вещественными числами, а также для представимости с помощью машин Блюм-Шуба-Смейла, работающих в бесконечном времени (ITBM-вычислимости). Особое внимание уделено вопросам существования таких представлений для несчётных структур и количества таких представлений. 

ВК
#матлог

--------------------------------------------------------------
Логика, лингвистика и формальная философия
1 ноября (суббота) в 18:00 (GMT+3) состоится заседание научно-учебного семинара «Математическая логика и теория категорий» (online).

Тема доклада: Abstract and Variable Sets in Category Theory.

Докладчик: John L. Bell (Emeritus Professor, FRSC Department of Philosophy Western University London, Ontario Canada).

Аннотация: In 1895 Cantor gave a definitive formulation of the concept of set, namely,
A collection to a whole of definite, well-differentiated objects of our intuition or thought.
Let us call such a collection a concrete set. More than a decade earlier, Cantor had introduced the notion of cardinal number by appeal to a process of abstraction:
If we abstract not only from the nature of the elements of a set, and also from the order in which they are given, then there arises in us a definite general concept which I call the cardinal number of the set.
Lawvere has suggested calling Cantor’s cardinal numbers abstract sets. An abstract set may be considered as arising from a concrete set when each element has been purged of all intrinsic qualities aside from the quality which distinguishes that element from all the others. An abstract set is thus an embodiment of pure discreetness.
In my talk I will describe how category theory provides the natural framework for understanding abstract sets, conceived of as static or as undergoing change.
_________________________

Ждём вас в кабинете А-117 или в Zoom!

Анонс и регистрация: https://llfp.hse.ru/announcements/1094081809.html

ВК
5
#матлог #учёба #спецсеминар

Семинар «Вероятностные и субструктурные логические системы» (www.mathnet.ru/conf2533) под руководством С.Л. Кузнецова (homepage.mi-ras.ru/~sk/) и С.О. Сперанского (homepage.mi-ras.ru/~speranski/).

Время: 30 октября (четверг), 16:00
Место: МИАН, ауд. 530 + Контур.Толк
 
В.А. Нестеров (МФТИ)
 
Название:
Верифицированное вычисление асимптотик вещественных функций (продолжение)
 
Аннотация:
Вычисление асимптотик функций - одна из нетривиальных математических задач, которая однако под силу компьютеру. Исследования в этом направлении были начаты Г. Харди и доведены до практического алгоритма Дж. Шекеллом в 1990 году.
 
В докладе я расскажу о своей имплементации алгоритма Шекелла (с некоторыми модификациями) в системе интерактивных доказательств Lean. Системы доказательств дают возможность писать доказательства на формальном языке с последующей автоматической проверкой компьютером. В своей работе я имплементировал алгоритм в виде так называемой тактики - программы, которая не только возвращает результат (например, предел функции на бесконечности), но и формальное доказательство его корректности (например, того, что функция действительно стремится к найденному значению). Такая тактика, будучи использованной как подпрограмма, позволяет сократить формальные доказательства других результатов в анализе и комбинаторике.
 
Если планируете посетить заседание (очно или онлайн через Контур.Толк), пожалуйста, зарегистрируйтесь по ссылке в верхней части страницы семинара:
 
https://www.mathnet.ru/conf2533

ВК
#матлог #учёба #спецсеминар

Семинар "Вычислимость и неклассические логики" работает по пятницам с 16.45 в аудитории 425.

31 октября 2025 г.

Г. Г. Черевиченко
"Номинальная унификация"
Унификация в простейшем случае — это решение уравнений в свободных алгебраических системах. Например, рассмотрим алфавит из двух символов a,b и уравнение aX=Yb, где X и Y обозначают слова в этом алфавите (которые надо найти). Слова с операцией приписывания образуют свободную полугруппу. Решение выглядит так: берём произвольное слово Z и полагаем X=Zb, Y=aZ, тогда aX=aZb=Yb. Мы как бы подобрали слово (aZb), подходящее под оба шаблона aX и Yb, от этого слово "унификация". В более хитрых случаях слова (например, формулы логики первого порядка или лямбда-термы) могут содержать связывающие операции (кванторы, лямбды) и рассматривать их надо с точностью до переименования связанных переменных. Проблема унификации в этом случае имеет неожиданное красивое решение.

ВК
#матлог #учёба #спецсеминар #отмены

6, 13 и 20 ноября заседаний семинара «Вероятностные и субструктурные логические системы» (www.mathnet.ru/conf2533) не будет.

Следующее заседание планируется 27 ноября.

ВК
👍1
#матлог

--------------------------------------------------------------
Логика, лингвистика и формальная философия
5 ноября в 18:10 состоится 104-е заседание научно-теоретического семинара «Формальная философия».

Тема доклада: Объекты "с секретами" по принципу "если - то" в экспериментах психологов.

Докладчик: Поддьяков Александр Николаевич (доктор психологических наук, ведущий научный сотрудник МЛ ЛогЛинФФ).

Аннотация: Один из путей познания новых объектов в самых разных областях – экспериментирование с ними на предмет выявления скрытых эффектов и зависимостей. Психологи занимаются экспериментированием с этим экспериментированием. Для своих экспериментов они создают разнообразные «проблемные ящики» с секретами, которые предлагают обследовать участникам – детям и взрослым. Сами объекты своей работой призваны удивлять, озадачивать, создавать условия для выдвижения гипотез, проб, ошибок и «ага»-реакций. Ведется наблюдение за этой деятельностью, выделяются стратегии и пр. В докладе будут рассмотрены особенности этих объектов в контексте их основной функции – делать наблюдаемыми некоторые составляющие мыслительной деятельности. В качестве демонстрационного материала будут представлены некоторые их таких объектов.
_____________________

Ждём вас в кабинете А-117 или в Zoom!

Анонс и регистрация: https://llfp.hse.ru/announcements/1097887604.html

ВК