Просьба ко всем участникам, в том числе смотрящим видеозаписи,
зарегистрироваться по этой ссылке.
Субструктурными логиками называются логические системы, в которых не принимаются все или некоторые из структурных правил: ослабления, перестановки, сокращения. Применения таких логических систем разнообразны. С их помощью моделируются рассуждения об ограниченных ресурсах: если формула $A$ задаёт некоторый ресурс, то она не эквивалентна «$A \textit{ и } A$», т. е. не выполнено правило сокращения.
Некоммутативные (без правила перестановки) субструктурные логики применяются для описания синтаксиса естественных языков, где играет роль порядок слов. Логики без правила ослабления (если $A$, то $B \to A$ для любого $B$) называются релевантными: в них моделируются рассуждения, где существенно должны использоваться все посылки. Таким образом, исключаются верные классически, но странные для естественного языка рассуждения вроде «Если завтра пойдёт дождь, то $2+2=4$». В рамках курса планируется дать общий обзор субструктурных логик и рассказать несколько наиболее ярких результатов об этих необычных логических системах.
Программа
- Секвенциальные исчисления для субструктурных логик: мультипликативно-аддитивное исчисление Ламбека и его расширения. Алгебраическая семантика: решётки с делениями.
- PSPACE-полнота задачи выводимости для мультипликативно-аддитивного исчисления Ламбека.
- Интерполяционная лемма Роорды для исчисления Ламбека. Теорема Пентуса о грамматиках Ламбека и контекстно-свободных грамматиках. Контрпример к теореме Пентуса для коммутативного случая.
- Теорема Андреки — Микулаша о полноте исчисления Ламбека относительно моделей на алгебрах бинарных отношений.
- Дистрибутивное мультипликативно-аддитивное исчисление Ламбека (по Козаку), его алгоритмическая разрешимость и свойство конечных моделей.
- Линейная логика Жирара. Консервативность классической линейной логики над интуиционистской (при отсутствии константы «ноль»).
- Алгоритмическая неразрешимость линейной логики и её некоммутативного мультипликативно-экспоненциального варианта.
- Релевантные логические системы, результаты Уркхарта об их алгоритмической неразрешимости.
- Неассоциативное исчисление Ламбека, тернарная семантика, полиномиальный алгоритм разрешения задачи выводимости.
- Исчисление Ламбека с итерацией Клини («логика действий») и его инфинитарный вариант. Результаты об алгоритмической неразрешимости.
 RSS: Ближайшие семинары
 Лекторы
Кузнецов Степан Львович
Пшеницын Тихон Григорьевич
Организации
Математический институт им. В.А. Стеклова Российской академии наук, г. Москва
Математический центр мирового уровня «Математический институт им. В.А. Стеклова Российской академии наук» (МЦМУ МИАН) |
