Спецкурс "Сложность исчисления Ламбека"

М. Р. Пентус
2006/2007

Программа спецкурса

Неассоциативное исчисление Ламбека, некоммутативная линейная логика, алгоритмические проблемы, понятие NP-сложности, понятие NP-полноты, доказательство NP-полноты мультипликативного фрагмента некоммутативной линейной логики, синтаксическое исчисление Ламбека, доказательство NP-полноты синтаксического исчисления Ламбека.

Краткое содержание прошедших лекций

        29.09.2006

Полиномиальный алгоритм проверки выводимости
в неассоциативном исчислении Ламбека без умножения
(Aarts, Trautwein, 1995).

Алгоритм Кока--Янгера--Касами
(the Cocke--Younger--Kasami algorithm, the CYK algorithm).
См., например, (Шень, 1995, задача 13.1.5),
(Хопкрофт, Мотвани, Ульман, 2002, пункт 7.4.4)
или главу "КС-языки и грамматики"
из конспекта "Основы компиляции" (авторы -- Д. В. Варсанофьев, А. Г. Дымченко).

        06.10.2006

Неассоциативное исчислении Ламбека NL
(de Groote, 1999).
Эквивалентность исчислений NL и NLH.
Корректность исчисления SC относительно NLH.

        13.10.2006

Вариант исчисления SC с тремя сортами секвенций.
Лемма о выводимости A->A в исчислении SC.
Лемма о построении вывода секвенции F[p<-E]->>p по выводам секвенций E->>p и F->>p.
Лемма о построении вывода секвенции p>->F[p<-E] по выводам секвенций p>->E и p>->F.
Лемма о построении вывода секвенции F->E\H по выводу секвенции F*E->H.

        20.10.2006

Лемма о построении вывода секвенции F*E->H по выводу секвенции F->E\H.
Полнота "трёхсортного" исчисления SC относительно NLH.
Полиномиальный алгоритм проверки выводимости
в неассоциативном исчислении Ламбека.

        03.11.2006

Некоммутативная линейная логика NCL.
Сети доказательства.

        10.11.2006

Сведение проблемы SAT к проблеме выводимости в NCL
(Pentus, 2006).
Аналог леммы 3.6 для NCL.
Аналог леммы 3.14 для NCL.
Домашнее задание:
(1) Ассоциативность мультипликативной дизъюнкции.
(2) Аналог леммы 3.2 для NCL.
(3) Аналог леммы 3.3 для NCL.

        17.11.2006

Аналог леммы 3.15 для NCL.
Домашнее задание:
(1) Аналог леммы 3.16 для NCL.

        24.11.2006

Мультипликативный фрагмент неассоциативного варианта исчисления BL2
(Lambek, 1993).
Симметрия.
Переворачивание стрелок.
Исчисления BL2, BL3 и другие варианты линейной логики
(только мультипликативные фрагменты).
Домашнее задание:
(1) Вывести B->A\C из A*B->C.
(2) Вывести A*B->C из B->A\C.

        01.12.2006

Свойства отображений symm и rev.
Три теоремы об эквивалентности 6 схем аксиом.
Правила про аддитивные связки, консервативность соответствующего расширения.
Гипотеза о консервативности расширения произвольной атомарной теории
квазипорядка посредством правил с новыми функциональными символами,
если не выводится симметричность этого квазипорядка.

        08.12.2006

Различные аксиоматизации мультипликативного фрагмента исчисления BL2.

        16.03.2007

Мультипликативная некоммутативная линейная логика.

        23.03.2007

Облегчённые сети доказательства
(Pentus, 2006).
3.3.2-3.3.7.

        30.03.2007

Облегчённые сети эквивалентности.
3.2.3, 3.2.4, 3.3.1, 3.4.1, 3.4.4.

        13.04.2007

Лемма о циклах в облегчённой сети эквивалентности.
3.4.5-3.4.8.

        27.04.2007

Леммы о простых формулах.
3.5.1-3.5.4.

        04.05.2007

Критерий эквивалентности неатомарной формулы атомарной формуле
в мультипликативной некоммутативной линейной логике.
3.5.4-3.5.6.

        11.05.2007

Экзамен.

Основная литература

Дополнительная литература


Адрес: http://lpcs.math.msu.su/~pentus/spec2006w.htm
Изменения внесены 04.05.2007.
Мати Рейнович Пентус
Телефон/факс: + 7 - 495 - 939 30 31