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

Logic Online Seminar, Monday 16:00 MSK (UTC+3), Room 313 MIAN + Kontur Talk (https://www.mathnet.ru/eng/conf876)

10 марта 2025 года

Тихон Пшеницын (МИАН, аспирант)
Интуиционистская линейная логика первого порядка и гиперграфовые языки (очный доклад)

Некоммутативные субструктурные логики имеют несколько точек соприкосновения с теорией формальных языков. С одной стороны, такие логики, например, исчисление Ламбека, используются как механизм задания формальных языков в категориальных грамматиках. С другой стороны, формальные языки возникают как модели субструктурных логик; основной результат в этом направлении, доказанный М.Р. Пентусом, гласит, что исчисление Ламбека корректно и полно относительно языковой семантики.

В докладе предполагается обсудить аналогичные взаимосвязи между субструктурными логиками первого порядка и гиперграфовыми языками. В первой части доклада будет предложено определение гиперграфовых L-грамматик, основанных на произвольной первопорядковой логике L (в секвенциальном формате). Оно обобщает понятие MILL1-грамматик — категориальных грамматик, основанных на мультипликативной интуиционистской линейной логике первого порядка MILL1. Последние рассматривались в работах [Μοοt, 2014], [Slavnov, 2023]. Будет показана связь гиперграфовых MILL1-грамматик, а также грамматик над интуиционистской линейной логикой первого порядка ILL1 с порождающими гиперграфовыми грамматиками. В качестве следствия будет дан ответ на открытый вопрос из [Moot, 2014] о классе языков, задаваемых строковыми MILL1-грамматиками; в частности, будет показано, что этот класс содержит NP-полный язык.

Во второй части доклада будет дано определение языковой семантики для логики MILL1, в рамках которой формулы интерпретируются гиперграфовыми языками, а мультипликативная конъюнкция (тензор) линейной логики интерпретируется операцией параллельной композиции. Эта операция хорошо известна в теории графовых грамматик в контексте HR-алгебр [Courcelle, 1990]. Будет установлена теорема о корректности и полноте для негативного фрагмента MILL1 (с помощью аналога конструкции [Buszkowski, 1982]). Вопрос полноты всей логики MILL1 относительно гиперграфово-языковой семантики остается открытым.

Доклад основан на препринте https://arxiv.org/abs/2502.05816.

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


➰ ВК