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

На занятии просеминара 12 декабря (последнем в 2024 году) будет продолжение темы "Деревья решений и вопросная сложность" (Н.К.Верещагин).
Можно заранее порешать задачи (прикреплены к посту).

❗По просьбам участников создан чат просеминара в телеграме:
https://t.me/+8lzSUf8ghLAzMjRi

Просеминар проходит по четвергам в 16:45-18:20 в аудитории 424 (2 гуманитарный корпус). Информацию о просеминаре можно найти на странице http://logic.math.msu.ru/proseminar/.

🔗 Просеминар по математической логике и информатике — Кафедра математической логики и теории алгоритмо


📝 Деревья решений и вопросная сложность 2024.pdf

➰ ВК

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

Logic Online Seminar (https://www.mathnet.ru/conf876) совместно с семинаром С.И. Адяна

понедельник 16:00 MSK (UTC+3), ауд. 313 МИАН + Контур Толк

16.12.2024 А.Я. Канель-Белов (Бар-Илан, МФТИ, МГУ, https://www.mathnet.ru/rus/person8698): Алгоритмическая неразрешимость проблемы вложения алгебраических многообразий (очный)

Чрезвычайно интересной и фундаментальной является задача об алгоритмической разрешимости проверки наличия изоморфизма между двумя алгебраическими многообразиями. Родственной и более простой задачей является задача о вложимости. В общем виде она формулируется так: пусть A и B – два алгебраических многообразия; определить, существует ли вложение A в B, найти алгоритм или доказать его отсутствие. Доклад посвящен отрицательному решению данного вопроса для аффинных многообразий над алгебраически замкнутым полем характеристики не 2, чьи координатные кольца заданы образующими и определяющими соотношениями.

🔗 Семинары отдела математической логики "Теория доказательств" и "Logic Online Seminar&


➰ ВК

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

Kolmogorov seminar on complexity (for receive the zoom link, please email nikolay.vereshchagin@gmail.com)

Date: Dec 16, 2024. Time: 18:30 (MSK), 16:30 (CET)
Speaker: Andrey Storozhenko, UCLA
Title: The communication complexity of approximating matrix rank (sequel)

It was shown that if Alice and Bob have n times n matrices A and B over a finite field, then deciding, if A + B have full rank requires n^2 log |F| bits, for deterministic protocols. Next time there will be a lower bound against randomized protocols (and probably for the approximate version of the problem).

➰ ВК

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

Уважаемые коллеги, приглашаем вас на последний в 2024 году логический семинар лаборатории им. Манина Высшей школы современной математики МФТИ (ВШМ).
Семинар пройдет в среду 18 декабря.
Время проведения семинара 14:30.

МФТИ, радиотехнический корпус, ауд. РТ 113
Институтский пер., 9, стр. 1, Долгопрудный

Ссылка на яндекс-карту с пешим маршрутом от ст. Новодачная:
https://yandex.ru/maps/213/moscow/?ll=37.519439%2C55.929820&mode=routes&rtext=55.924397%2C37.527944~55.929869%2C37.516242&rtt=mt&ruri=ymapsbm1%3A%2F%2Ftransit%2Fstop%3Fid%3Dstation__lh_9601261~ymapsbm1%3A%2F%2Forg%3Foid%3D1109621791&utm_source=share&z=16

В здании пропускной режим, поэтому если у вас нет пропуска в МФТИ, то напишите на почту (kudinov.andrey@gmail.com) заранее.

Заседание пройдет очно без трансляции.

Докладчик: Андрей Кудинов

Название: О сохранение сложности слаботранзитивных модальных логик с универсальной модальностью при добавлении аксиомы связности.

Аннотация.

Под сложностью проблемы выполнимости некоторой модальной логики L понимается сложность следующей массовой задачи: по данной формуле A определить, выполнима ли формула A на некоторой шкале логики L. Эта задача является двойственной к задачи выводимости в логике, т.к. формула A выводима в L тогда и только тогда, когда формула \lnot A невыполнима на L-шкале. Сложностной класс PSPACE содержит все массовые задачи, которые можно решить на машине Тьюринга, которая использует не больше полинома от длины входа ячеек ленты в процессе выполнения.

Мы будем рассматривать слаботранзитивные логики, т.е. логики содержащие wK4 = K + \Box p \land p \to \Box \Box p.
Общезначимость этой логики соответствует тому, что рефлексивное замыкание отношения - транзитивно.
Добавление универсальной модальности увеличивает выразительную силу языка. Добавление универсальной модальности рассматривалось в 90-е годы в работах Горанко и Пасси, а в работе Шехтмана было доказано, что в языке с универсальной модальностью можно выразить связность.

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

➰ ВК

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

Семинар «Теория доказательств» / Logic Online Seminar (https://www.mathnet.ru/conf876)
понедельник 16:00 MSK (UTC+3), ауд. 313 МИАН + Контур Толк

23.12.2024 М.В. Валинкин (МГУ, https://www.mathnet.ru/person196590) и С.Л. Кузнецов (МИАН, https://www.mathnet.ru/person72238): Реляционные модели для исчисления Ламбека с субэкспоненциалом нелокального сокращения (очный доклад)

Исчисление Ламбека является субструктурной логикой, в которой отсутствуют правила сокращения, ослабления и даже перестановки. Одним из естественных классов моделей для исчисления Ламбека являются модели на алгебрах бинарных отношений (R-модели). Субэкспоненциалы — это модальности, добавляемые к субструктурным логикам, под знаком которых разрешены некоторые из этих правил. В рамках доклада будут рассмотрены расширения исчисления Ламбека с помощью субэкспоненциала, допускающего правило сокращения соседних формул (локального сокращения), в нескольких вариантах. Такой субэкспоненциал имеет естественную интерпретацию в R-моделях, поскольку условие локального сокращения соответствует свойству отношения быть плотным. Будут изложены доказательства теорем о полноте относительно R-моделей для рассматриваемых исчислений.

🔗 Семинары отдела математической логики "Теория доказательств" и "Logic Online Seminar&


➰ ВК

#матлог #конфереция #ВМК

Факультет вычислительной математики и кибернетики Московского государственного университета им. М.В. Ломоносова приглашает Вас принять участие в однодневной научно-практической конференции, посвящённой 100-летию со дня рождения создателя троичных ЭВМ Николая Петровича Брусенцова, которая состоится 7 февраля 2025 года по адресу: Москва, Ленинские горы, МГУ им. М.В. Ломоносова, 2-й учебный корпус, факультет ВМК, аудитория П-8а.

Начало регистрации – 13-30, начало докладов – 14-00.

Основные темы конференции:
• история создания и использования троичных машин, сохранение наследия;
• математические исследования, связанные с троичным представлением чисел и логических отношений;
• перспективы использования троичной вычислительной техники и алгоритмов.

Все необходимые для участия в конференции материалы размещены на интернет-странице по адресу: http://ternarycomp.cs.msu.ru/100.html.

Для регистрации на конференции используйте, пожалуйста, страницу https://conf.msu.ru/rus/event/9380/ или сообщите о намерении участвовать на адрес brusentsov100@cs.msu.ru.

📝 Конференция 100 лет Брусенцову.pdf

➰ ВК

#матлог
Празднуем день логики!

--------------------------------------------------------------
↪ Логика, лингвистика и формальная философия

15 января состоится Российско-бразильский коллоквиум по логическому плюрализму, приуроченный ко Всемирному дню логики.

https://llfp.hse.ru/announcements/1001702478.html

🔗 Всемирный день логики


➰ ВК

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

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

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

Семинар пройдет в формате ZOOM, для получения ссылки пишите на почту kudinov.andrey@gmail.com.

Видео докладов выкладываются на канале: https://www.youtube.com/channel/UC_Aq6N03uRgVkEcvS6lJLog

Докладчик: Тихон Пшеницын

Название: Введение в гиперарифметическую иерархию

Аннотация:

Многим известна арифметическая иерархия, которая классифицирует неразрешимые множества, задаваемые арифметическими формулами первого порядка. Также на слуху аналитическая иерархия, определяемая аналогичным образом с помощью логики второго порядка. Однако менее популярна гиперарифметическая иерархия, которая заполняет пробел между арифметической и аналитической иерархиями. В гиперарифметической иерархии определяются уровни Σ^0_α и Π^0_α не только для натуральных α, но и для всех конструктивных ординалов. Мы начнем с аккуратного введения гиперарифметической иерархии, обсудим ее основные свойства. Будет приведен пример Σ^0_α-полного множества вычислимых инфинитарных формул в простейшем языке (эти формулы строятся из констант "истина" и "ложь" с помощью вычислимых конъюнкций и дизъюнкций). После этого будет приведено несколько примеров логик, задача выводимости в которых имеет гиперарифметический уровень сложности (эти результаты получены в работах С.Л. Кузнецова, С.О. Сперанского и докладчика, в том числе в соавторстве).

🔗 Логика в Москве


➰ ВК

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

Уважаемые коллеги, приглашаем вас на логический семинар лаборатории им. Манина Высшей школы современной математики МФТИ (ВШМ).
Семинар пройдет в среду 22 января.
Время проведения семинара 14:30.

‼Важно ‼ Если у вас нет пропуска в МФТИ, то нужно до обеда 21 января (вторник) написать на почту kudinov.andrey@gmail.com, чтобы мы успели заказать пропуск. Пропускной режим ужесточился!

МФТИ, радиотехнический корпус, ауд. РТ 113
Институтский пер., 9, стр. 1, Долгопрудный

Ссылка на яндекс-карту с пешим маршрутом от ст. Новодачная:
https://yandex.ru/maps/213/moscow/?ll=37.519439%2C55.929820&mode=routes&rtext=55.924397%2C37.527944~55.929869%2C37.516242&rtt=mt&ruri=ymapsbm1%3A%2F%2Ftransit%2Fstop%3Fid%3Dstation__lh_9601261~ymapsbm1%3A%2F%2Forg%3Foid%3D1109621791&utm_source=share&z=16

Заседание пройдет очно без трансляции.

Докладчик: Михаил Рыбаков

Название:
Алгоритмическая выразительность модальных предикатных логик, определяемых неэлементарными классами шкал Крипке.

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

➰ ВК

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

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

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

Семинар пройдет в формате ZOOM, для получения ссылки пишите на почту kudinov.andrey@gmail.com.

Видео докладов выкладываются на канале:
https://www.youtube.com/channel/UC_Aq6N03uRgVkEcvS6lJLog

Докладчик: Александр Грефенштейн (МИАН)

Название:
Инфинитарное исчисление для вероятностной логики Кейслера–Хувера над дискретными пространствами

Аннотация:

Вероятностная логика Кейслера–Хувера (точнее, её версия без счётных конъюнкций и дизъюнкций) получается из классической логики первого порядка посредством замены обычных кванторов всеобщности и существования на «вероятностные кванторы» вида (Px = q), где q бегает по рациональным числам. В основе её семантики лежат первопорядковые структуры с вероятностными распределениями на носителе; при этом (Px = q) Φ(x) означает, что вероятность того, что x удовлетворяет Ф(x), больше или равна q. Известно, что данная логика имеет высокую степень алгоритмической неразрешимости: соответствующая ей проблема общезначимости является \Pi^1_1-трудной, даже если ограничиться лишь дискретными вероятностными распределениями. В докладе будет представлено сильно полное инфинитарное (содержащее \omega-правила, т.е. правила со счётным числом посылок) исчисление для логики Кейслера–Хувера над дискретными пространствами. Особое внимание будет уделено тому, как конструкция Хенкина переносится на случай инфинитарного исчисления, оперирующего финитарными формулами, и как из полученной с помощью такой конструкции «слабой» модели с конечно-аддитивной мерой получается настоящая модель с вероятностной мерой.

🔗 Логика в Москве


➰ ВК

#матлог #учёба #спецкурс

Д.ф.-м.н., акад. Л.Д. Беклемишев прочитает спецкурс НОЦ МИАН "Введение в теорию моделей, часть II".

Первая лекция: 12 февраля

Место проведения: МИАН, ком. 303

Время проведения: среда 16:00-17:30

Страница спецкурса: https://www.mathnet.ru/conf2535

Аннотация.
В первой части курса, прочитанного в НОЦ МИАН в 2024 году (https://www.mathnet.ru/conf2376), остались не покрытыми некоторые важные темы базового курса теории моделей. Мы планируем рассказать об этих вопросах в данном курсе. В качестве кульминации мы планируем изложить доказательство знаменитой теоремы Морли о категоричности.

Программа:
- Метод элементарных цепей.
- Насыщенные и однородные модели.
- Критерии аксиоматизируемости теорий ограниченными классами формул (∀∃-формулами, позитивными формулами, хорновскими формулами).
- Элементарная теория вещественно замкнутых полей, её полнота и разрешимость, 17-я проблема Гильберта.
- Теорема Морли о категоричности.

🔗 Курс Л. Д. Беклемишева "Введение в теорию моделей, часть II"


➰ ВК

#матлог #учёба #спецкурс

Д.ф.-м.н. С.Л. Кузнецов и асп. Т.Г. Пшеницын прочитают спецкурс НОЦ МИАН "Субструктурные логики".

Первая лекция: 13 февраля

Место проведения: МИАН, ком. 313

Время проведения: четверг 16:00-17:30

Страница спецкурса: https://www.mathnet.ru/conf2538

Аннотация.
Субструктурными логиками называются логические системы, в которых не принимаются все или некоторые из структурных правил: ослабления, перестановки, сокращения. Применения таких логических систем разнообразны. С их помощью моделируются рассуждения об ограниченных ресурсах: если формула A задаёт некоторый ресурс, то она не эквивалентна «A и A», т. е. не выполнено правило сокращения.

Некоммутативные (без правила перестановки) субструктурные логики применяются для описания синтаксиса естественных языков, где играет роль порядок слов. Логики без правила ослабления (если A, то B→A для любого B ) называются релевантными: в них моделируются рассуждения, где существенно должны использоваться все посылки. Таким образом, исключаются верные классически, но странные для естественного языка рассуждения вроде «Если завтра пойдёт дождь, то 2+2=4 ». В рамках курса планируется дать общий обзор субструктурных логик и рассказать несколько наиболее ярких результатов об этих необычных логических системах.

Программа

- Секвенциальные исчисления для субструктурных логик: мультипликативно-аддитивное исчисление Ламбека и его расширения. Алгебраическая семантика: решётки с делениями.
- PSPACE-полнота задачи выводимости для мультипликативно-аддитивного исчисления Ламбека.
- Интерполяционная лемма Роорды для исчисления Ламбека. Теорема Пентуса о грамматиках Ламбека и контекстно-свободных грамматиках. Контрпример к теореме Пентуса для коммутативного случая.
- Теорема Андреки — Микулаша о полноте исчисления Ламбека относительно моделей на алгебрах бинарных отношений.
- Дистрибутивное мультипликативно-аддитивное исчисление Ламбека (по Козаку), его алгоритмическая разрешимость и свойство конечных моделей.
- Линейная логика Жирара. Консервативность классической линейной логики над интуиционистской (при отсутствии константы «ноль»).
- Алгоритмическая неразрешимость линейной логики и её некоммутативного мультипликативно-экспоненциального варианта.
- Релевантные логические системы, результаты Уркхарта об их алгоритмической неразрешимости.
- Неассоциативное исчисление Ламбека, тернарная семантика, полиномиальный алгоритм разрешения задачи выводимости.
- Исчисление Ламбека с итерацией Клини («логика действий») и его инфинитарный вариант. Результаты об алгоритмической неразрешимости.

🔗 Курс С. Л. Кузнецова и Т. Г. Пшеницына "Субструктурные логики"


➰ ВК

#матлог #учёба #спецкурс

Д.ф.-м.н. И.Г. Лысенок прочитает спецкурс НОЦ МИАН "Введение в геометрическую теорию групп".

Первая лекция: 10 февраля

Место проведения: МИАН, ком. 430

Время проведения: понедельник 18:00-19:30

Страница спецкурса: https://www.mathnet.ru/conf2531

Аннотация.
Цель спецкурса — ознакомление слушателей с ключевыми понятиями и методами геометрической теории групп. В частности, будет дано представление о теории групп, действующих на деревьях (теории Басса-Серра), квазиизометрических отображениях пространств, гиперболических метрических пространствах и гиперболических группах в смысле Громова. От участников спецкурса не требуется специальной подготовки, достаточно лишь знания алгебры в объёме университетского курса, а также начальных понятий топологии. Приглашаются студенты любых курсов и аспиранты.

Программа

- Свободные группы.
Определение свободной группы. Лемма о ромбе. Нормальная форма элементов. Универсальное свойство свободных групп.
- Задания групп с помощью порождающих и соотношений.
Выводы с помощью определяющих соотношений групп. Алгебраическая интерпретация заданий групп с помощью фактор-групп свободных групп. Преобразования Тице. Диаграммы ван Кампена. Лемма ван Кампена.
- Введение в алгоритмические проблемы.
Проблемы равенства и сопряженности. Проблема сопряженности в свободных группах. Проблема изоморфизма. Пример класса групп с разрешимой проблемой изоморфизма: конечно порожденные абелевы группы. Проблема вхождения в подгруппу. Неразрешимость большинства алгоритмических проблем для групп (без доказательства).
- Графы в геометрической теории групп.
Графы как комбинаторные 1-комплексы. Деревья. Фундаментальная группа графа. Накрытия графов. Действия групп: основные понятия. Графы Кэли и Шрайера. Теорема Шрайера о подгруппах свободной группы. Проблема вхождения в подгруппу для свободной группы.
- Асимптотические характеристики групп.
Словарная метрика на группе. Функция роста. Инвариантность функции роста относительно выбора порождающих групп. Функция Дэна. Инвариантность функции Дэна относительно выбора задания группы в терминах порождающих и соотношений. Примеры верхних оценок функции Дэна.
- Свободные конструкции.
Свободные произведения групп. Нормальная форма элементов свободного произведения. Универсальное свойство свободного произведения. Свободные произведения с объединенной подгруппой. Модифицированный вариант леммы о ромбе. Нормальная форма элементов свободного произведения с объединенной подгруппой. Универсальное свойство свободного произведения с объединенной подгруппой. HNN-расширения групп. Нормальная форма элементов HNN-расширения. Лемма Бриттона.
- Введение в теорию групп, действующих на деревьях.
Графы групп. Построение фундаментальной группы графа групп. Построение дерева действия группы для свободных конструкций. Построение дерева действия групп в общем случае.
- Введение в грубую геометрию.
Квазиизометричечкие вложения. Квазиизометрии. Критерии квазиизометричности. Теорема Милнора-Шварца. Квазиизометрические инварианты групп.
- Гиперболические метрические пространства.
Геодезические пространства. Метрические деревья. Эквивалентные определения гиперболических метрических пространств.
- Гиперболические группы.
Теорема Громова об эквивалетности гиперболичности группы линейности ее функции Дэна. Примеры гиперболических групп: дискретные подгруппы движений гиперболического пространства; группы с условием малого сокращения.

🔗 Курс И. Г. Лысёнка "Введение в геометрическую теорию групп"


➰ ВК

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

В МИАН будет работать семинар «Вероятностные и субструктурные логические системы» (рук. С.Л. Кузнецов и С.О. Сперанский), ориентированный на студентов и аспирантов.

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

Место проведения: МИАН, ком. 303

Время проведения: вторник 16:00-17:30

Страница спецсеминара: https://www.mathnet.ru/conf2533

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

Субструктурные логики — это логические системы, в которых не принимаются все или некоторые из структурных правил. Такие логики используются для моделирования вычислений с ограниченными ресурсами (ресурс, в отличие от математического утверждения, нельзя использовать повторно), а их некоммутативные версии находят применения в математической лингвистике. Инфинитарные расширения субструктурных логик обладают интересными алгоритмическими и теоретико-доказательственными свойствами.

Предварительная программа
Предполагаемый формат семинара — доклады продолжительностью в 2–4 занятия. Каждый доклад будет посвящён некоторой вероятностной или субструктурной логической системе и включать разбор доказательств сопутствующих результатов. Докладчики будут выбираться руководителями семинара, в основном из числа студентов и аспирантов.
В качестве источников могут выступать статьи и главы из книг, а также собственные тексты докладчиков.

🔗 Семинар С. Л. Кузнецова и С. О. Сперанского "Вероятностные и субструктурные логические системы&


➰ ВК

#матлог #учёба #спецкурс

В этом семестре Станислав Сперанский будет читать курс «Введение в неклассические логики». Этот курс читается в рамках Базовой кафедры МИАН в МФТИ, однако посещать его могут все желающие.

Первая лекция: 11 февраля

Место проведения: МИАН, ауд. 430

Время проведения: вторник 14:15-15:40

Страница курса: https://www.mathnet.ru/conf2543

Аннотация:

Данный курс представляет собой доступное введение в неклассические логики. Традиционно всякая логика, отличная от классической, называется «неклассической». Существует много разнообразных неклассических логик, которые применяются в основаниях математики, информатике, формальной философии и эпистемологии, лингвистике и т.д. Практически невозможно дать обзор большинства из них в рамках одного курса. Поэтому вместо того, чтобы пытаться рассмотреть настолько много логик, насколько возможно, мы сосредоточимся на определённых фундаментальных вопросах и методах, связанных с неклассическими логиками. Более того, хотя существуют различные виды семантики для неклассических логик, нас будет в основном интересовать так называемая семантика Крипке, также известная как реляционная семантика или семантика возможных миров. Этот вид семантики адекватным образом отражает интуицию, стоящую за большинством неклассических логик, и имеет динамический характер: здесь в основе структур лежат множества «миров», или «информационных состояний», связанных между собой посредством «отношений достижимости».

Особое место в данном курсе занимают интуиционистская логика и (классическая) модальная логика, обозначаемые через Int и K соответственно:

— Поведение связки импликации в Int сильно отличается от поведения классической, «материальной» импликации. На самом деле, интуиционистская импликация имеет более конструктивный и в определённом смысле интуитивный характер. Так, в Int исчезают многие из так называемых парадоксов классической импликации.

— В языке K, помимо символов языка классической логики, присутствуют дополнительные символы модальных операторов «необходимо, что» и «возможно, что»; при этом немодальные логические символы ведут себя классически. Таким образом, K обогащает классическую логику, не меняя смысла стандартных связок. Модальные операторы играют ключевую роль в применениях формальной логики в информатике и лингвистике. Например, в естественном языке оператору «возможно, что» соответствует модальный глагол «мочь»: грубо говоря, предложение «Он может написать книгу» равносильно предложению «Возможно, что он напишет книгу».

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

🔗 Открытые лекции по теме «Введение в неклассические логики»


➰ ВК

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

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

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

Семинар пройдет в формате ZOOM, для получения ссылки пишите на почту kudinov.andrey@gmail.com.

Видео докладов выкладываются на канале:
https://www.youtube.com/channel/UC_Aq6N03uRgVkEcvS6lJLog

Докладчик: Павел Разумный

Название: Об алгоритмической сложности логики QGL, расширенной нефундированными выводами

Аннотация: Будет рассматриваться логика QGL_inf - предикатная версия логики Гёделя-Лёба, расширенная нефундированными выводами. Мы докажем, что при достаточно богатой сигнатуре (а именно, содержащей 4 унарных, 3 бинарных и 1 тернарный предикатных символов) к множеству теорем этой логики сводится задача о неостановке машины Тьюринга; из этого факта легко выводится неперечислимость множества теорем QGL_inf.
Также будет доказана эквивалентность логики QGL_inf логике QGL c омега-правилом Лёба (обобщение обычного правила Лёба); с помощью данной эквивалентности будет получена верхняя оценка сложности: класс Sigma^1_1 аналитической иерархии.

🔗 Логика в Москве


➰ ВК

#матлог #наука #спецсеминар

The Proof Society Seminar (https://www.proofsociety.org/proof-theory-seminar/index.html) presents talks by leading researchers in proof theory and from all areas of logic related to proofs. We are affiliated with the Proof Society, and our aims with this seminar are closely aligned with the Proof Society's Manifesto, particularly in enabling communication within the broader scientific community. Everyone who is interested in the subject is warmly invited to attend!

The talks take place online via Zoom, usually on Mondays, approximately once per month. They start at 13:00 UTC and may last up to 75 minutes plus questions.

The seminar organizer is Lev D. Beklemishev (levbekl@gmail.com). The seminar board consists of the committee members of the Proof Society.

03 February 2025, 13:00 UTC

Jeremy Avigad (Carnegie Mellon University)

Verifying Proofs on Blockchain

In cryptography, a *club227889084 (*proof) system* is a protocol between a prover and a verifier that enables the prover to convince the verifier that a claim is true. They are often probabilistic; given a source of randomness, it is often more efficient to convince the verifier only that it is very likely that the claim is true. Such proof systems now have interesting applications to blockchain technology, where they are used, among other things, to validate the execution of smart contracts.

It is easy to make mistakes when implementing cryptographic protocols and designing smart contracts, and billions of dollars are lost to hacks every year. Fortunately, another proof technology can help: interactive proof assistants, which have long been used to verify hardware and software systems, can also be used to verify the correctness of cryptographic protocols.

In this talk, I will describe some formal verification efforts I have carried out with colleagues at StarkWare Industries using the Lean proof assistant. I will explain some of the ideas behind smart contracts and interactive proof assistants without assuming familiarity with either.

🔗 Proof Theory Virtual Seminar - Home


➰ ВК

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

Уважаемые коллеги, приглашаем вас на логический семинар лаборатории им. Манина Высшей школы современной математики МФТИ (ВШМ).
Семинар пройдет в среду 5 февраля.
Время проведения семинара 14:30.

‼Если у вас нет пропуска в МФТИ, то нужно заранее написать на почту kudinov.andrey@gmail.com.

МФТИ, радиотехнический корпус, ауд. РТ 113
Институтский пер., 9, стр. 1, Долгопрудный

Ссылка на яндекс-карту с пешим маршрутом от ст. Новодачная:
https://yandex.ru/maps/213/moscow/?ll=37.519439%2C55.929820&mode=routes&rtext=55.924397%2C37.527944~55.929869%2C37.516242&rtt=mt&ruri=ymapsbm1%3A%2F%2Ftransit%2Fstop%3Fid%3Dstation__lh_9601261~ymapsbm1%3A%2F%2Forg%3Foid%3D1109621791&utm_source=share&z=16

Заседание пройдет очно без трансляции.

Докладчик: Стас Кикоть

Название: О дихотомии для модальных логик некоторых элементарных классов шкал Крипке

В докладе рассматриваются нормальные модальные логики элементарных классов, определяемых формулами первого порядка вида ∀x0 ∃x1 · · · ∃xn C, где C - конъюнкция бинарных атомов от этих переменных. Оказывается, что многие свойства этих логик, такие как конечная аксиоматизируемость, элементарность, аксиоматизируемость набором канонических формул или одной обобщенной формулой Салквиста, вместе с модальной определимостью исходной формулы, либо одновременно выполняются, либо одновременно не выполняются. Будет представлен простой теоретико-графовый критерий для определения того, какой из этих случаев имеет место. Этот критерий связан с совместной работой с Евгением Золиным об ответах на модально определимые конъюнктивные запросы в дескрипционных логиках.

➰ ВК

#матлог #учёба #спецкурс

В этом семестре в МГУ (при поддержке Фонда «БАЗИС») будет читаться курс С.О. Сперанского «Проблемы алгоритмической разрешимости теорий для алгебры и анализа».

Первая лекция: 14 февраля

Место проведения: МГУ, ауд. 1414

Время проведения: пятница, 16:45-18:20

Страница курса (где можно найти расширенную аннотацию и предварительный план лекций):

https://homepage.mi-ras.ru/~speranski/courses/theories.html

Аннотация:

Теории классов структур в языке логики первого порядка традиционно называют «элементарными»; они являются одним из основных объектов изучения в математической логике и теории алгоритмов. Элементарная теория данного класса — это совокупность свойств, выразимых в соответствующем языке и присущих всем структурам из класса; её алгоритмическая разрешимость означает возможность эффективной проверки «элементарных» свойств над рассматриваемым классом. Многие известные результаты, а также открытые проблемы в математической логике связаны с изучением вычислительных аспектов элементарных теорий различных классов групп, колец и т.п. и их естественных фрагментов. Это классическое и не теряющее актуальности направление исследований, восходящее к фундаментальным работам А. Тарского и А.И. Мальцева.

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

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

❗ Просьба ко всем участникам зарегистрироваться через Google-форму, ссылка на которую есть в верхней части страницы курса — см. кнопку «Регистрация».

🔗 Станислав Сперанский


➰ ВК

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

UPD: The forthcoming talk on February 10th (Monday) will be given by Prof. Aleksandar Perović (University of Belgrade, https://www.scopus.com/authid/detail.uri?authorId=23987185400), who is another co-author of the work.

Logic Online Seminar, Monday 16:00 MSK (UTC+3), Room 313 MIAN + Kontur Talk (https://www.mathnet.ru/eng/conf876)
10.02.2025 Angelina Ilić-Stepić (Matematički institut SANU, Beograd, Srbija, https://www.mi.sanu.ac.rs/novi_sajt/members/fulltime/angelina.php): Beyond the class of locally finite height Kripke models for provability logic (online)

The paper [K. Sasaki & Y. Tanaka 2024: An omega-rule for the logic of provability and its models, Studia Logica 112] presents the propositional logic NGL, an extension of the provability logic GL with an infinitary inference rule, and proves simple completeness theorem w.r.t. the class LF of locally finite height Kripke models. We provide a strongly complete modification of NGL and a family of Barwise-complete infinitary logics that correspond to specific subclasses of the class of all conversely well-founded strict posets that are proper superclasses of LF.

The talk is based on joint work with Zoran Ognjanović and Aleksandar Perović.

🔗 Seminars "Proof Theory" and "Logic Online Seminar"


➰ ВК