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

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

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

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

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

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

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

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

Программа

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

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


➰ ВК