Автоматическое доказательство теорем в линейной логике

Является ли автоматическое доказательство теорем и поиск доказательств более простым в линейных и других пропозициональных субструктурных логиках, в которых отсутствует сжатие?

Где я могу прочитать больше об автоматическом доказательстве теорем в этих логиках и роли сокращения в поиске доказательства?

Другие ресурсы могут быть найдены ссылки в диссертации Kaustuv Чоудхури в « сфокусированного Обратный метод линейной логики », и вы можете быть заинтересованы в Рой Dyckhoff в « Сужение-Free Sequent исчислений », который о сокращении , но не о линейной логики.

Существуют возможности для эффективного поиска доказательств в линейной логике, но я не думаю, что текущая работа показывает, что это проще, чем поиск доказательств в не субструктурной логике. Проблема в том, что если вы хотите доказать в линейной логике, у вас есть дополнительный вопрос, которого у вас нет при обычном поиске доказательства: используется для доказательства или используется для доказательства ? На практике этот «недетерминированность ресурсов» является большой проблемой при выполнении поиска доказательств в линейной логике.C A C $C \vdash(A \otimes B)$$C$$A$$C$$B$

Согласно комментариям, Lincoln et al., 1990 " Задачи решения для пропозициональной линейной логики ", является хорошим справочным материалом, если вы хотите получить техническую информацию о таких словах, как "проще".

Нет, все сложнее.

Точно так же, как задача решения для интуиционистской логики высказываний сложнее, чем для классической логики высказываний, линейная логика высказываний еще сложнее. С экспонентами (которые не испытывают недостатка в сжатии) или с различными разновидностями некоммутативного связующего, логика становится неразрешимой, и даже слабый классический МОЛЛ является завершенным PSPACE. В отличие от этого, задача решения для классической логики высказываний завершена совместно с NP, а для интуиционистской логики высказываний - завершена PSPACE. (Необязательно, я не знаю сложности интуитивного МОЛЛА.)

Я рекомендую описание Пэта Линкольна в разделе 6 его линейной логики , SIGACT News 1992. С тех пор мы узнали немного больше, то есть у нас есть результаты для большого семейства линейных логик, но основная картина есть.

Определенным образом это то, что делает поиск доказательств линейной логики интересным, поскольку сложность решения проблемы создает пространство для более интересных представлений о вычислениях, а линейная логика сложна во многих отношениях. Андрей указал на « Обзор линейного логического программирования» Дейла Миллера ; это хорошее место, чтобы посмотреть, так как Миллер сделал больше, чтобы развить идею поиска доказательства как вычисление, как кто-либо еще.

Предполагая, что сложность проблемы доказуемости удовлетворит вас, ландшафт сложностей субструктурной логики с сокращением и без него несколько сложен. Я попытаюсь рассмотреть здесь то, что известно пропозициональной линейной логикой и пропозициональной логикой. Короткий ответ заключается в том, что сокращение иногда помогает (например, LLC является разрешимым, в то время как LL - нет), а иногда нет (например, MALL является PSPACE-полным, MALLC является ACKERMANN-полным).

Логика высказываний

• CL: классическая логика
• IL: интуиционистская логика
• LL: линейная логика, фрагменты MLL (мультипликативные), MELL (мультипликативные экспоненциальные), MALL (мультипликативные аддитивные)
• LLW: аффинная логика, т.е. LL с ослаблением, те же фрагменты, что и выше
• LLC: сжимающая линейная логика, т.е. LL с сокращением, те же фрагменты, что и выше
• $_\to$$_{\to,\wedge}$

Сложность Обеспечиваемости

• NP-полная: MLL [Kan91]
• совместная NP-полная: CL
• PSPACE-полный: IL [Sta79], МОЛЛ [Lin92]
• $_\to$
• БАШНЯ полная: MELLW, LLW [Laz14]
• $_{\to,\wedge}$
• $\Sigma_1^0$

$_\to$

Ссылки

• [Kan91] Макс Канович, Мультипликативный фрагмент линейной логики является NP-полным , Исследовательский отчет X-91-13, Институт языка, логики и информации, 1991.
• [Laz14] Ранко Лазич и Сильвен Шмитц, Неэлементарные сложности для ветвления VASS, MELL и расширений , рукопись, 2014. arXiv: 1401.6785 [cs.LO]
• [Lin92] Патрик Линкольн, Джон Митчелл, Андре Счедров и Натараджан Шанкар, Проблемы принятия решений для линейной логики высказываний , Анналы чистой и прикладной логики 56 (1–3): 239–311, 1992. 10.1016 / 0168-0072 (92) 90075-B
• [Sch14] Сильвен Шмитц, Логика импликационных релевантностей, полная 2-ExpTime , рукопись, 2014. arXiv: 1402.0705 [cs.LO]
• [Sta79] Ричард Стэтман, Интуиционистская логика высказываний полна в пространстве , Теоретическая компьютерная наука 9 (1): 67–72, 1979. doi: 10.1016 / 0304-3975 (79) 90006-9
• [Urq84] Аласдейр Уркхарт, «Неразрешимость последствий и соответствующие последствия» , Журнал символической логики 49 (4): 1059–1073, 1984. doi: 10.2307 / 2274261
• [Urq99] Аласдэр Уркхарт, Сложность процедур принятия решений в логике релевантности II , Журнал символической логики 64 (4): 1774–1802, 1999. 10.2307 / 2586811

Возможно, Дейл Миллер Обзор линейного логического программирования - это хорошая точка отсчета?