Линейная логика

Линейная логика — это субструктурная логика, предложенная французским логиком Жан-Ивом Жираром как усовершенствование классической и интуиционистской логики , объединяющая двойственность первой со многими конструктивными свойствами последней. ^[1] Хотя логика также изучалась сама по себе, в более широком смысле идеи линейной логики оказали влияние на такие области, как языки программирования , семантика игр и квантовая физика (поскольку линейную логику можно рассматривать как логику квантовой теории информации ). , ^[2] а также лингвистика , ^[3] особенно из-за его акцента на ограниченности ресурсов, двойственности и взаимодействии.

Линейная логика допускает множество различных представлений, объяснений и интуиций. С точки зрения теории доказательства оно вытекает из анализа классического секвенциального исчисления , в котором использование ( структурных правил ) сжатия и ослабления тщательно контролируется. С практической точки зрения это означает, что логический вывод больше не является просто постоянно расширяющейся коллекцией устойчивых «истин», но также и способом манипулирования ресурсами , которые не всегда можно дублировать или выбрасывать по своему желанию. С точки зрения простых денотационных моделей линейную логику можно рассматривать как усовершенствованную интерпретацию интуиционистской логики путем замены декартовых (замкнутых) категорий или симметричными моноидальными (замкнутыми) категориями интерпретацию классической логики путем замены булевых алгебр C *-алгебрами . ^{[ нужна ссылка ]}

и полярность , двойственность Связи

Синтаксис [ править ]

Язык классической линейной логики (CLL) определяется индуктивно с помощью обозначения BNF.

$А$	::=	$п ∣ п ⊥$
	$∣$	$А \otimes А ∣ А \oplus А$
	$∣$	$А и А ∣ А ⅋ А$
	$∣$	$1 ∣ 0 ∣ ⊤ ∣ ⊥$
	$∣$	$! А ∣ ? А$

Здесь $п$ и $п ⊥$ диапазон над логическими атомами . По причинам, которые будут объяснены ниже, связки ⊗, ⅋, 1 и ⊥ называются мультипликативами , связки &, ⊕, ⊤ и 0 называются аддитивами , а связки ! и ? называются экспонентами . Далее мы можем использовать следующую терминологию:


Символ	Имя
⊗	мультипликативный союз	раз	тензор
⊕	аддитивная дизъюнкция	плюс
&	аддитивный союз	с
⅋	мультипликативная дизъюнкция	для
!	конечно	хлопнуть
?	почему нет	квест

Бинарные связки ⊗, ⊕, & и ⅋ ассоциативны и коммутативны; 1 — единица измерения ⊗, 0 — единица измерения ⊕, ⊥ — единица измерения ⅋, а ⊤ — единица измерения &.

Каждое предложение $A$ в CLL имеет двойственное $A. ⊥$ , определяемый следующим образом:

$(п) ⊥ = п ⊥$			$(п ⊥) ⊥ = п$
$(А \otimes Б) ⊥ = А ⊥ ⅋ Б ⊥$			$(А ⅋ Б) ⊥ = А ⊥ \otimes Б ⊥$
$(А \oplus Б) ⊥ = А ⊥ & Б ⊥$			$(А и Б) ⊥ = А ⊥ \oplus Б ⊥$
$(1) ⊥ = ⊥$			$(⊥) ⊥ = 1$
$(0) ⊥ = ⊤$			$(⊤) ⊥ = 0$
$(! А) ⊥ = ?(А ⊥)$			$(? А) ⊥ = !(А ⊥)$

Классификация связок
	добавлять	у меня есть	опыт
позиция	⊕ 0	⊗ 1	!
нег	& ⊤	⅋ ⊥	?

Обратите внимание, что $(-) ⊥$ является инволюцией , т. е. $A ⊥⊥ = A$ для всех предложений. $А ⊥$ называется линейным отрицанием A $.$ также

Столбцы таблицы предлагают другой способ классификации связок линейной логики, называемый полярность : отрицательные связки в левом столбце (⊗, ⊕, 1, 0, !) называются положительными , а двойственные им справа (⅋, &, ⊥, ⊤, ?) называются отрицательными ; ср. стол справа.

Линейная импликация не включена в грамматику связок, но в CLL ее можно определить с помощью линейного отрицания и мультипликативной дизъюнкции по формуле $A ⊸ B := A. ⊥ ⅋ Б.$ Соединительный союз ⊸ иногда произносится как « леденец » из-за его формы.

Презентация исчисления последовательного

Один из способов определения линейной логики — это секвенциальное исчисление . Мы используем буквы $Γ$ и $Δ$ ранжирования списков предложений $A 1, ..., An для$ , также называемых контекстами . Секвенция турникета помещает контекст слева и справа от , записанный $\vdash$ . Интуитивно секвенция утверждает, что конъюнкция $Γ$ влечет за собой дизъюнкцию $Δ$ (хотя мы имеем в виду «мультипликативную» конъюнкцию и дизъюнкцию, как поясняется ниже). Жирар описывает классическую линейную логику, используя только односторонние секвенции (где левый контекст пуст), и мы следуем здесь этому более экономичному изложению. Это возможно, поскольку любое помещение слева от турникета всегда можно перенести на другую сторону и дуализировать.

Теперь мы дадим правила вывода, описывающие, как строить доказательства секвенций. ^[4]

Во-первых, чтобы формализовать тот факт, что нас не волнует порядок предложений внутри контекста, мы добавляем структурное правило обмена :

\vdash

\vdash

Обратите внимание, что мы не добавляем структурные правила ослабления и сокращения, поскольку нас заботит отсутствие предложений в секвенции и количество присутствующих копий.

Далее мы добавляем начальные секвенции и разрезы :

\vdash

$\vdash$			$\vdash$

$\vdash$

Правило отсечения можно рассматривать как способ составления доказательств, а начальные секвенции служат единицами композиции . В определенном смысле эти правила избыточны: поскольку ниже мы вводим дополнительные правила для построения доказательств, мы будем сохранять то свойство, что произвольные начальные секвенции могут быть получены из атомарных начальных секвенций и что всякий раз, когда секвенция доказуема, ей можно дать разрез. бесплатное доказательство. В конечном счете, это свойство канонической формы (которое можно разделить на полноту атомарных начальных секвенций и теорему об исключении разреза , порождающую понятие аналитического доказательства ) лежит в основе приложений линейной логики в информатике, поскольку оно позволяет логике быть с учетом ресурсов используется при поиске доказательств и в качестве лямбда-исчисления .

Теперь мы объясним связки, приведя логические правила . Обычно в секвенциальном исчислении для каждой связки даются как «правые правила», так и «левые правила», по существу описывая два способа рассуждения о предложениях, включающих эту связку (например, проверка и фальсификация). В одностороннем представлении вместо этого используется отрицание: правые правила для связки (скажем, ⅋) эффективно играют роль левых правил для ее двойственной (⊗). Итак, следует ожидать определенной «гармонии» между правилом(ами) для связки и правилом(ами) для ее двойственного.

Мультипликативы [ править ]

Правила мультипликативного конъюнкции (⊗) и дизъюнкции (⅋):

$\vdash$			$\vdash$

$\vdash$

\vdash

\vdash

и для их подразделений:



$\vdash$

\vdash

\vdash

Заметим, что правила мультипликативной конъюнкции и дизъюнкции допустимы для простой конъюнкции и дизъюнкции в классической интерпретации.(т.е. они являются допустимыми правилами в LK ).

Добавки [ править ]

Правила аддитивной конъюнкции (&) и дизъюнкции (⊕):

$\vdash$			$\vdash$

$\vdash$

\vdash

\vdash

\vdash

\vdash

и для их подразделений:



$\vdash$

(нет правила для

0

)

Заметим, что правила аддитивной конъюнкции и дизъюнкции снова допустимы в классической интерпретации. Но теперь мы можем объяснить основу мультипликативного/аддитивного различия в правилах для двух разных вариантов конъюнкции: для мультипликативной связки (⊗) контекст заключения ( $Γ, Δ$ ) расщепляется между посылками, тогда как для аддитивной падежной связки (&) контекст заключения ( $Γ$ ) целиком переносится в обе посылки.

Экспоненты [ править ]

Экспоненты используются для обеспечения контролируемого доступа к ослаблению и сокращению. В частности, мы добавляем структурные правила ослабления и сокращения для $?$ есть предложения: ^[5]

\vdash

\vdash

\vdash

\vdash

и используйте следующие логические правила:

\vdash

\vdash

\vdash

\vdash

Можно заметить, что правила для экспонент следуют иной схеме, чем правила для других связок, напоминая правила вывода, управляющие модальностями в последовательных формализациях исчисления нормальной модальной логики S4 , и что больше нет такой явной симметрии между двойники $!$ и $?$ . Эта ситуация исправляется в альтернативных представлениях CLL (например, в представлении LU ).

Замечательные формулы [ править ]

Помимо описанных выше двойственностей Де Моргана , некоторые важные эквивалентности в линейной логике включают:

Дистрибутивность

А \otimes (B \oplus C) ≣ (А \otimes B) \oplus (А \otimes C)

(А \oplus B) \otimes C ≣ (А \otimes C) \oplus (B \otimes C)

А ⅋ (Б и С) ≣ (А ⅋ Б) & (А ⅋ С)

(А и Б) ⅋ С ≣ (А ⅋ С) & (Б ⅋ С)

По определению $A ⊸ B$ как $A ⊥ ⅋ B$ два последних закона распределения также дают:

А ⊸ (B & C) ≣ (А ⊸ B) & (А ⊸ C)

(А \oplus B) ⊸ C ≣ (А ⊸ C) & (B ⊸ C)

(Здесь $A ≣ B$ есть $(A ⊸ B) & (B ⊸ A)$ .)

Экспоненциальный изоморфизм

!(А и Б) ≣ ! А \otimes ! Б

?(А \oplus B) ≣ ? А ⅋ ? Б

Линейные распределения

Отображение, которое не является изоморфизмом, но играет решающую роль в линейной логике:

(А \otimes (B ⅋ C)) ⊸ ((А \otimes B) ⅋ C)

Линейные распределения являются фундаментальными в теории доказательств линейной логики. Последствия этой карты были впервые исследованы в ^[6] и называется «слабым распределением». В последующей работе оно было переименовано в «линейное распределение», чтобы отразить фундаментальную связь с линейной логикой.

Другие последствия

Следующие формулы дистрибутивности, как правило, не являются эквивалентностью, а являются лишь импликацией:

! А \otimes ! Б ⊸ !(А \otimes Б)

! А \oplus ! Б ⊸ !(А \oplus Б)

?(А ⅋ B) ⊸ ? А ⅋ ? Б

?(А и В) ⊸ ? А & ? Б

(А и B) \otimes C ⊸ (А \otimes C) & (B \otimes C)

(А и B) \oplus C ⊸ (А \oplus C) & (B \oplus C)

(А ⅋ C) \oplus (B ⅋ C) ⊸ (А \oplus B) ⅋ C

(А и С) \oplus (Б и С) ⊸ (А \oplus Б) и С

классической/интуиционистской логики в логику Кодирование линейную

Как интуиционистскую, так и классическую импликацию можно восстановить из линейной импликации путем вставки экспонент: интуиционистская импликация кодируется как $! A ⊸ B$ , а классическую импликацию можно закодировать как $!? А ⊸ ? Б$ или $! А ⊸?! B$ (или множество альтернативных возможных переводов). ^[7] Идея состоит в том, что экспоненты позволяют нам использовать формулу столько раз, сколько нам нужно, что всегда возможно в классической и интуиционистской логике.

Формально существует перевод формул интуиционистской логики в формулы линейной логики таким образом, чтобы гарантировать доказуемость исходной формулы в интуиционистской логике тогда и только тогда, когда переведенная формула доказуема в линейной логике. Таким образом, используя отрицательный перевод Гёделя – Генцена , мы можем встроить классическую логику первого порядка в линейную логику первого порядка.

Интерпретация ресурса [ править ]

Лафонт (1993) первым показал, как интуиционистскую линейную логику можно объяснить как логику ресурсов, предоставив таким образом логическому языку доступ к формализмам, которые можно использовать для рассуждений о ресурсах внутри самой логики, а не, как в классической логике, путем средствами нелогических предикатов и отношений. Тони Хоара Классический пример торгового автомата (1985) можно использовать для иллюстрации этой идеи.

Предположим, мы представляем наличие шоколадного батончика атомарным предложением $candy$ , а наличие доллара — $1 долларом$ . Чтобы констатировать тот факт, что за доллар вы сможете купить одну шоколадку, мы могли бы написать импликацию $$1 \Rightarrow конфета$ . в обычной (классической или интуиционистской) логике из $A$ и $A \Rightarrow B$ можно заключить $A \land B.$ Но Итак, обычная логика приводит нас к мысли, что мы можем купить шоколадку и сохранить свой доллар! Конечно,мы можем избежать этой проблемы, используя более сложные кодировки, ^{[ нужны разъяснения ]} хотя обычно такие кодировки страдают от проблем с кадрами . Однако отказ от ослабления и сжатия позволяет линейной логике избежать такого рода ложных рассуждений даже при наличии «наивного» правила. Вместо $$1 \Rightarrow candy$ мы выражаем свойство торгового автомата как линейную импликацию $$1 ⊸ candy$ . Из $$1$ и этого факта мы можем сделать вывод $о конфетах$ , но не $о $1 \otimes конфетах$ . В общем, мы можем использовать предложение линейной логики $A ⊸ B,$ выразить обоснованность преобразования ресурса $A$ в ресурс $B.$ чтобы

На примере торгового автомата рассмотрим «ресурсные интерпретации» других мультипликативных и аддитивных связок. (Экспоненты предоставляют средства для объединения этой интерпретации ресурса с обычным понятием устойчивой логической истины .)

Мультипликативный союз $(A \otimes B)$ обозначает одновременное появление ресурсов, которые будут использоваться по указанию потребителя. Например, если вы покупаете жевательную резинку и бутылку безалкогольного напитка, вы запрашиваете $резинку \otimes жевательную$ . Константа 1 обозначает отсутствие какого-либо ресурса и поэтому действует как единица ⊗.

Аддитивный союз $(А и Б)$ представляет собой альтернативное возникновение ресурсов, выбор которых контролирует потребитель. Если в торговом автомате есть пачка чипсов, шоколадный батончик и банка безалкогольного напитка, каждая из которых стоит один доллар, то за эту цену вы можете купить ровно один из этих продуктов. Таким образом, мы пишем $$1 ⊸ (конфеты, чипсы и напитки)$ . Мы не пишем $1 доллар ⊸ (конфеты \otimes чипсы \otimes напиток)$ , что означало бы, что одного доллара достаточно для покупки всех трех продуктов вместе. Однако из $$1 ⊸ (конфеты, чипсы и напитки)$ мы можем правильно вывести $$3 ⊸ (конфеты \otimes чипсы \otimes напиток)$ , где $$3 := $1 \otimes $1 \otimes $1$ . Единицу ⊤ аддитивного соединения можно рассматривать как мусорную корзину для ненужных ресурсов. Например, мы можем написать $$3 ⊸ (конфеты \otimes ⊤),$ чтобы выразить, что за три доллара вы можете получить шоколадный батончик и некоторые другие вещи, не вдаваясь в подробности (например, чипсы и напиток, или 2 доллара, или 1 доллар и фишки). , и т. д.).

Аддитивная дизъюнкция $(A \oplus B)$ представляет собой альтернативное появление ресурсов, выбором которых управляет машина. Например, предположим, что торговый автомат разрешает азартные игры: вставьте доллар, и автомат сможет выдать шоколадный батончик, пачку чипсов или безалкогольный напиток. Мы можем выразить эту ситуацию как $1 доллар ⊸ (конфеты \oplus чипсы \oplus напиток)$ . Константа 0 представляет продукт, который невозможно произвести, и, таким образом, служит единицей ⊕ (машина, которая может производить $А$ или $0$ , так же хороша, как и машина, которая всегда производит $А,$ потому что ей никогда не удастся произвести 0). Таким образом, в отличие от предыдущего, мы не можем вывести $из этого 3 доллара ⊸ (конфеты \otimes чипсы \otimes напиток)$ .

системы доказательств Другие

Доказательственные сети [ править ]

Сети доказательств , предложенные Жан-Ивом Жираром , были созданы во избежание бюрократии , то есть всего того, что делает два вывода разными с логической точки зрения, но не с «моральной» точки зрения.

Например, эти два доказательства «морально» идентичны:

\vdash

\vdash

\vdash

\vdash

\vdash

\vdash

Цель сетей доказательств — сделать их идентичными, создав их графическое представление.

Семантика [ править ]

Алгебраическая семантика [ править ]

Разрешимость/сложность следствия [ править ]

Отношение следования в полной CLL неразрешимо . ^[8] При рассмотрении фрагментовCLL, проблема решения имеет различную сложность:

Мультипликативная линейная логика (MLL): только мультипликативные связки. Следствие MLL является NP-полным , даже ограничиваясь предложениями Хорна в чисто импликативном фрагменте, ^[9] или к безатомным формулам. ^[10]
Мультипликативно-аддитивная линейная логика (MALL): только мультипликативы и добавки (т. е. безэкспоненциально). MALL является PSPACE-полным . ^[8]
Мультипликативно-экспоненциальная линейная логика (MELL): только мультипликативы и экспоненты. Путем редукции из проблемы достижимости сетей Петри , ^[11] Следствие MELL должно быть как минимум EXPSPACE-трудным , хотя сама разрешимость имеет статус давней открытой проблемы. В 2015 году доказательство разрешимости было опубликовано в журнале Theoretical Computer Science . ^[12] но позже выяснилось, что это ошибочно. ^[13]
В 1995 году было показано, что аффинная линейная логика (то есть линейная логика с ослаблением, расширением, а не фрагментом) разрешима. ^[14]

Варианты [ править ]

Многие варианты линейной логики возникают в результате дальнейшего изменения структурных правил:

Аффинная логика , которая запрещает сокращение, но допускает глобальное ослабление (разрешимое расширение).
Строгая логика или соответствующая логика , которая запрещает ослабление, но допускает глобальное сжатие.
Некоммутативная логика или упорядоченная логика, которая устраняет правило обмена, а также запрещает ослабление и сжатие. В упорядоченной логике линейная импликация делится на левую и правую импликацию.

Рассмотрены различные интуиционистские варианты линейной логики. Когда оно основано на представлении последовательного исчисления с одним выводом, как в ILL (интуиционистская линейная логика), связки ⅋, ⊥ и ? отсутствуют, а линейная импликация трактуется как примитивная связка. В FILL (полная интуиционистская линейная логика) связки ⅋, ⊥ и ? присутствуют, линейная импликация является примитивной связкой и, подобно тому, что происходит в интуиционистской логике, все связки (кроме линейного отрицания) независимы.Существуют также расширения линейной логики первого и высшего порядка, формальное развитие которых несколько стандартно (см. Логика первого порядка и логика высшего порядка ).

См. также [ править ]

Ссылки [ править ]

^ Жирар, Жан-Ив (1987). «Линейная логика» (PDF) . Теоретическая информатика . 50 (1): 1–102. дои : 10.1016/0304-3975(87)90045-4 . hdl : 10338.dmlcz/120513 .
^ Баэз, Джон ; Останься, Майк (2008). Боб Коке (ред.). «Физика, топология, логика и вычисления: Розеттский камень» (PDF) . Новые структуры физики .
^ де Пайва, В .; ван Генабит, Дж.; Риттер, Э. (1999). Семинар Дагштуля 99341 по линейной логике и приложениям (PDF) . стр. 1–21. дои : 10.4230/DagSemRep.248 .
^ Жирар (1987), стр.22, Def.1.15
^ Жирар (1987), стр.25-26, Def.1.21
^ Дж. Робин Кокетт и Роберт Сили «Слабо дистрибутивные категории» Журнал чистой и прикладной алгебры 114 (2) 133-173, 1997
^ Ди Космо, Роберто. Букварь по линейной логике . Конспекты курса; глава 2.
^ Jump up to: Перейти обратно: ^а ^б Этот результат и обсуждение некоторых приведенных ниже фрагментов см.: Линкольн, Патрик; Митчелл, Джон; Щедров, Андре; Шанкар, Натараджан (1992). «Проблемы принятия решений для пропозициональной линейной логики» . Анналы чистой и прикладной логики . 56 (1–3): 239–311. дои : 10.1016/0168-0072(92)90075-Б .
^ Канович, Макс И. (22 июня 1992 г.). «Горновое программирование в линейной логике NP-полно». Седьмой ежегодный симпозиум IEEE по логике в информатике, 1992. LICS '92. Слушания . Седьмой ежегодный симпозиум IEEE по логике в информатике , 1992. LICS '92. Слушания. стр. 200–210. дои : 10.1109/LICS.1992.185533 . ISBN 0-8186-2735-2 .
^ Линкольн, Патрик; Винклер, Тимоти (1994). «Мультипликативная линейная логика, состоящая только из констант, является NP-полной» . Теоретическая информатика . 135 : 155–169. дои : 10.1016/0304-3975(94)00108-1 .
^ Гюнтер, Калифорния; Гелот, В. (1989). Сети как тензорные теории (PDF) (Технический отчет). Пенсильванский университет. МС-СНГ-89-68.
^ Бимбо, Каталин (13 сентября 2015 г.). «Разрешимость интенсионального фрагмента классической линейной логики» . Теоретическая информатика . 597 : 1–17. дои : 10.1016/j.tcs.2015.06.019 . ISSN 0304-3975 .
^ Страсбургер, Лутц (10 мая 2019 г.). «О решении проблемы для MELL» . Теоретическая информатика . 768 : 91–98. дои : 10.1016/j.tcs.2019.02.022 . ISSN 0304-3975 .
^ Копылов, А.П. (1 июня 1995 г.). «Разрешимость линейной аффинной логики». Десятый ежегодный симпозиум IEEE по логике в информатике, 1995. LICS '95. Слушания . Десятый ежегодный симпозиум IEEE по логике в информатике, 1995. LICS '95. Слушания. стр. 496–504. CiteSeerX 10.1.1.23.9226 . дои : 10.1109/LICS.1995.523283 . ISBN 0-8186-7050-9 .

Дальнейшее чтение [ править ]

Жирар, Жан-Ив. Линейная логика , Теоретическая информатика, Том 50, № 1, стр. 1–102, 1987.
Жирар, Жан-Ив, Лафон, Ив и Тейлор, Поль. Доказательства и типы . Кембридж Пресс, 1989.
Хоар, ЦАР, 1985. Обмен последовательными процессами . Прентис-Холл Интернэшнл. ISBN 0-13-153271-5
Лафон, Ив, 1993. Введение в линейную логику . Конспекты лекций летней школы TEMPUS по алгебраическим и категориальным методам в информатике , Брно, Чехия.
Троэльстра А.С. Лекции по линейной логике . CSLI (Центр изучения языка и информации). Конспект лекций № 29. Стэнфорд, 1992.
А.С. Троэльстра , Х. Швихтенберг (1996). Основная теория доказательств . В серии «Кембриджские трактаты по теоретической информатике» , издательство Кембриджского университета, ISBN 0-521-77911-1 .
Ди Космо, Роберто и Данос, Винсент. Букварь по линейной логике .
Введение в линейную логику (Постскриптум) Патрика Линкольна
Введение в линейную логику Торбена Браунера
Вкус линейной логики от Филиппа Уодлера
Линейная логика Роберто Ди Космо и Дейла Миллера . Стэнфордская энциклопедия философии (выпуск осенью 2006 г.), Эдвард Н. Залта (ред.).
Обзор линейного логического программирования Миллера Дейла . В книге «Линейная логика в информатике» под редакцией Эрхарда, Жирара, Рюэ и Скотта. Издательство Кембриджского университета. Конспект лекций Лондонского математического общества, том 316, 2004 г.
Линейная логика вики

Внешние ссылки [ править ]

СМИ, связанные с линейной логикой, на Викискладе?
Доказательство линейной логики (llprover). Архивировано 4 апреля 2016 г. на Wayback Machine , доступно для использования в Интернете по адресу: Наоюки Тамура / Кафедра компьютерных наук / Университет Кобе / Япония.

[1] Жирар, Жан-Ив (1987). «Линейная логика» (PDF) . Теоретическая информатика . 50 (1): 1–102. дои : 10.1016/0304-3975(87)90045-4 . hdl : 10338.dmlcz/120513 .

[2] Баэз, Джон ; Останься, Майк (2008). Боб Коке (ред.). «Физика, топология, логика и вычисления: Розеттский камень» (PDF) . Новые структуры физики .

[3] де Пайва, В .; ван Генабит, Дж.; Риттер, Э. (1999). Семинар Дагштуля 99341 по линейной логике и приложениям (PDF) . стр. 1–21. дои : 10.4230/DagSemRep.248 .

[4] Жирар (1987), стр.22, Def.1.15

[5] Жирар (1987), стр.25-26, Def.1.21

[6] Дж. Робин Кокетт и Роберт Сили «Слабо дистрибутивные категории» Журнал чистой и прикладной алгебры 114 (2) 133-173, 1997

[7] Ди Космо, Роберто. Букварь по линейной логике . Конспекты курса; глава 2.

[Lincoln+92-8] Jump up to: Перейти обратно: ^а ^б Этот результат и обсуждение некоторых приведенных ниже фрагментов см.: Линкольн, Патрик; Митчелл, Джон; Щедров, Андре; Шанкар, Натараджан (1992). «Проблемы принятия решений для пропозициональной линейной логики» . Анналы чистой и прикладной логики . 56 (1–3): 239–311. дои : 10.1016/0168-0072(92)90075-Б .

[9] Канович, Макс И. (22 июня 1992 г.). «Горновое программирование в линейной логике NP-полно». Седьмой ежегодный симпозиум IEEE по логике в информатике, 1992. LICS '92. Слушания . Седьмой ежегодный симпозиум IEEE по логике в информатике , 1992. LICS '92. Слушания. стр. 200–210. дои : 10.1109/LICS.1992.185533 . ISBN 0-8186-2735-2 .

[10] Линкольн, Патрик; Винклер, Тимоти (1994). «Мультипликативная линейная логика, состоящая только из констант, является NP-полной» . Теоретическая информатика . 135 : 155–169. дои : 10.1016/0304-3975(94)00108-1 .

[11] Гюнтер, Калифорния; Гелот, В. (1989). Сети как тензорные теории (PDF) (Технический отчет). Пенсильванский университет. МС-СНГ-89-68.

[12] Бимбо, Каталин (13 сентября 2015 г.). «Разрешимость интенсионального фрагмента классической линейной логики» . Теоретическая информатика . 597 : 1–17. дои : 10.1016/j.tcs.2015.06.019 . ISSN 0304-3975 .

[13] Страсбургер, Лутц (10 мая 2019 г.). «О решении проблемы для MELL» . Теоретическая информатика . 768 : 91–98. дои : 10.1016/j.tcs.2019.02.022 . ISSN 0304-3975 .

[14] Копылов, А.П. (1 июня 1995 г.). «Разрешимость линейной аффинной логики». Десятый ежегодный симпозиум IEEE по логике в информатике, 1995. LICS '95. Слушания . Десятый ежегодный симпозиум IEEE по логике в информатике, 1995. LICS '95. Слушания. стр. 496–504. CiteSeerX 10.1.1.23.9226 . дои : 10.1109/LICS.1995.523283 . ISBN 0-8186-7050-9 .

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

v т и Неклассическая логика
интуиционистский	Интуиционистская логика Конструктивный анализ Хейтинговая арифметика Интуиционистская теория типов Конструктивная теория множеств
Нечеткий	Степень правды Нечеткое правило Нечеткий набор Нечеткий конечный элемент Операции с нечетким множеством
субструктурный	Структурное правило Логика релевантности Линейная логика
Парапоследовательный	Диалетеизм
Описание	Онтология (информатика) Язык онтологий
Многозначный	Трехзначный Четырехзначный Лукасевич
Цифровая логика	Логика трех состояний Буфер с тремя состояниями Четырехзначный Верилог ИЭЭЭ 1164 VHDL
Другие	Динамическая семантика Пытливая логика Промежуточная логика Немонотонная логика