Linear logic: Difference between revisions

Revision as of 03:38, 13 October 2022

Latest revision as of 10:22, 20 May 2025

(30 intermediate revisions by 21 users not shown)

Line 1:

{{Short description|System of resource-aware logic}}

{{use dmy dates|date=March 2025}}

{{Redirect|⅋|the EP|⅋ (EP)}}

{{Redirect|⅋|the EP|& (The Moth & The Flame EP){{!}}''&'' (The Moth & The Flame EP)}}

'''Linear logic''' is a [[substructural logic]] proposed by [[Jean-Yves Girard]] as a refinement of [[classical logic|classical]] and [[intuitionistic logic]], joining the [[Duality (mathematics)|dualities]] of the former with many of the [[Constructivism (mathematics)|constructive]] properties of the latter.<ref>{{cite journal|last1=Girard|first1=Jean-Yves|year=1987|title=Linear logic|url=http://girard.perso.math.cnrs.fr/linear.pdf|journal=Theoretical Computer Science|volume=50|issue=1|pages=1–102|doi=10.1016/0304-3975(87)90045-4|hdl=10338.dmlcz/120513|author1-link=Jean-Yves Girard|doi-access=free}}</ref> Although the logic has also been studied for its own sake, more broadly, ideas from linear logic have been influential in fields such as [[programming languages]], [[game semantics]], and [[quantum physics]] (because linear logic can be seen as the logic of [[quantum information theory]]),<ref>{{cite journal|first1=John|last1=Baez|author1-link=John Baez|first2=Mike|last2=Stay|year=2008|title=Physics, Topology, Logic and Computation: A Rosetta Stone|editor=Bob Coecke|editor-link=Bob Coecke|journal=New Structures of Physics|url=http://math.ucr.edu/home/baez/rosetta.pdf}}</ref> as well as [[linguistics]],<ref>{{cite book|title=Dagstuhl Seminar 99341 on Linear Logic and Applications|first1=V.|last1=de Paiva|author1-link= Valeria de Paiva |first2=J.|last2=van Genabith|first3=E.|last3=Ritter|year=1999|url=http://www.dagstuhl.de/Reports/99/99341.pdf}}</ref> particularly because of its emphasis on resource-boundedness, duality, and interaction.

'''Linear logic''' is a [[substructural logic]] proposed by French [[logician]] [[Jean-Yves Girard]] as a refinement of [[classical logic|classical]] and [[intuitionistic logic]], joining the [[Duality (mathematics)#Duality in logic and set theory|dualities]] of the former with many of the [[Constructivism (mathematics)|constructive]] properties of the latter.{{sfn|Girard|1987}} Although the logic has also been studied for its own sake, more broadly, ideas from linear logic have been influential in fields such as [[programming languages]], [[game semantics]], and [[quantum physics]] (because linear logic can be seen as the logic of [[quantum information theory]]),{{sfn|Baez|Stay|2008}} as well as [[linguistics]],{{sfn|De Paiva|Van Genabith|Ritter|1999}} particularly because of its emphasis on resource-boundedness, duality, and interaction.

Linear logic lends itself to many different presentations, explanations, and intuitions.

Line 7 ⟶ 8:

==Connectives, duality, and polarity==

===Syntax===

{{anchor|Classical linear logic}}

The language of ''classical linear logic'' (CLL) is defined inductively by the [[Backus–Naur form|BNF notation]]

Line 34 ⟶ 35:

|}

Here {{math|<VAR>p</VAR>}} and {{math|<VAR>p</VAR>^⊥}} range over [[Atomic formula|logical atoms]]. For reasons to be explained below, the [[Logical connective|connectives]] ⊗, ⅋, 1, and ⊥ are called ''multiplicatives'', the connectives &, ⊕, ⊤, and 0 are called ''additives'', and the connectives ! and ? are called ''exponentials''.

We can further employ the following terminology:

over [[Atomic formula|logical atoms]]. For reasons to be explained

below, the [[Logical connective|connectives]] ⊗, ⅋, 1, and

⊥ are called ''multiplicatives'', the connectives &,

⊕, ⊤, and 0 are called ''additives'', and the

connectives ! and ? are called ''exponentials''. We can further

employ the following terminology:

{| class="wikitable"

|+

Line 59 ⟶ 56:

| colspan="2" |with

|-

|{{Anchor|⅋}}⅋

|multiplicative [[Logical disjunction|disjunction]]

| colspan="2" |par

Line 68 ⟶ 65:

|-

|?

| colspan="3" |why not

| colspan="3" |quest

|}

Binary connectives ⊗, ⊕, & and ⅋ are associative and commutative; 1 is the unit for ⊗, 0 is the unit for ⊕, ⊥ is the unit for ⅋ and ⊤ is the unit for &.

Every proposition {{math|<VAR>A</VAR>}} in CLL has a '''dual''' {{math|<VAR>A</VAR>^⊥}}, defined as follows:

{| border="1" cellpadding="5" cellspacing="0" style="margin:auto"

|-

Line 108 ⟶ 107:

| & ⊤ || ⅋ ⊥ || ?

|}

Observe that {{math|(-)^⊥}} is an [[Involution (mathematics)|involution]], i.e., {{math|<VAR>A</VAR>^⊥⊥ {{=}} <VAR>A</VAR>}} for all propositions. {{math|<VAR>A</VAR>^⊥}} is also called the ''linear negation'' of {{math|<VAR>A</VAR>}}.

The columns of the table suggest another way of classifying the connectives of linear logic, termed '''{{em|{{visible anchor|polarity}}}}''': the connectives negated in the left column (⊗, ⊕, 1, 0, !) are called ''positive'', while their duals on the right (⅋, &, ⊥, ⊤, ?) are called ''negative''; cf. table on the right.

''{{em|{{visible anchor|Linear implication''}}}} is not included in the grammar of connectives, but is definable in CLL using linear negation and multiplicative disjunction, by {{math|<VAR>A</VAR> ⊸ <VAR>B</VAR> :{{=}} <VAR>A</VAR>^⊥ ⅋ <VAR>B</VAR>}}. The connective ⊸ is sometimes pronounced "[[lollipop]]", owing to its shape.

==Sequent calculus presentation==

One way of defining linear logic is as a [[sequent calculus]]. We use the letters {{math| Γ}} and {{math| Δ}} to range over listlists of propositions {{math|<VAR>A</VAR>₁, ..., <VAR>A</VAR>_''n''}}, also called ''contexts''. A ''sequent'' places a context to the left and the right of the [[turnstile (symbol)|turnstile]], written {{math|Γ {{tee}} Δ}}. Intuitively, the sequent asserts that the conjunction of {{math| Γ}} [[Logical consequence|entails]] the disjunction of {{math| Δ}} (though we mean the "multiplicative" conjunction and disjunction, as explained below). Girard describes classical linear logic using only ''one-sided'' sequents (where the left-hand context is empty), and we follow here that more economical presentation. This is possible because any premises to the left of a turnstile can always be moved to the other side and dualised.

We now give [[Sequent calculus#Inference rules|inference rules]] describing how to build proofs of sequents.<ref>{{sfn|Girard (|1987), |loc=p.22, Def.1.15</ref>}}

First, to formalize the fact that we do not care about the order of propositions inside a context, we add the structural rule of [[exchange rule|exchange]]:

[[exchange rule|exchange]]:

{| style="margin:auto" border="0"

Line 132 ⟶ 131:

|}

Note that we do '''not''' add the structural rules of weakening and contraction, because we do care about the absence of propositions in a sequent, and the number of copies present.

absence of propositions in a sequent, and the number of copies present.

Next we add ''initial sequents'' and ''cuts'':

{| style="margin:auto"

|-

Line 159 ⟶ 158:

|}

The cut rule can be seen as a way of composing proofs, and initial sequents serve as the [[identity element|units]] for composition. In a certain sense these rules are redundant: as we introduce additional rules for building proofs below, we will maintain the property that arbitrary initial sequents can be derived from atomic initial sequents, and that whenever a sequent is provable it can be given a cut-free proof.

for composition. In a certain sense these rules are redundant: as we introduce additional rules for building proofs below, we will maintain the property that arbitrary initial sequents can be derived from atomic initial sequents, and that whenever a sequent is provable it can be given a cut-free proof. Ultimately, this [[canonical form]] property (which can be divided into the [[completeness of atomic initial sequents]] and the [[cut-elimination theorem]], inducing a notion of [[analytic proof]]) lies behind the applications of linear logic in computer science, since it allows the logic to be used in proof search and as a resource-aware [[lambda-calculus]].

Now, we explain the connectives by giving ''logical rules''. Typically in sequent calculus one gives both "right-rules" and "left-rules" for each connective, essentially describing two modes of reasoning about propositions involving that connective (e.g., verification and falsification).

In a one-sided presentation, one instead makes use of negation: the right-rules for a connective (say ⅋) effectively play the role of left-rules for its dual (⊗).

one gives both "right-rules" and "left-rules" for each connective, essentially describing two modes of reasoning

So, we should expect a certain [[Logical harmony|"harmony"]] between the rule(s) for a connective and the rule(s) for its dual.

about propositions involving that connective (e.g., verification and falsification). In a one-sided presentation, one instead makes use of negation: the right-rules for a connective

(say ⅋) effectively play the role of left-rules for its dual (⊗). So, we should expect a certain [[Logical harmony|"harmony"]]

between the rule(s) for a connective and the rule(s) for its dual.

===Multiplicatives===

The rules for multiplicative conjunction (⊗) and disjunction (⅋):

{| style="margin:auto"

|-

Line 195 ⟶ 193:

and for their units:

{| style="margin:auto"

|-

Line 218 ⟶ 217:

|}

Observe that the rules for multiplicative conjunction and disjunction are [[Admissible rule|admissible]] for plain ''conjunction'' and ''disjunction'' under a classical interpretation

plain ''conjunction'' and ''disjunction'' under a classical interpretation

(i.e., they are admissible rules in [[Sequent calculus#The system LK|LK]]).

Line 225 ⟶ 223:

The rules for additive conjunction (&) and disjunction (⊕) :

{| style="margin:auto"

|-

Line 257 ⟶ 256:

|}

|}

and for their units:

{| style="margin:auto"

|-

Line 273 ⟶ 274:

|}

Observe that the rules for additive conjunction and disjunction are again admissible under a classical interpretation.

But now we can explain the basis for the multiplicative/additive distinction in the rules for the two different versions of conjunction: for the multiplicative connective (⊗), the context of the conclusion ({{math|Γ, Δ}}) is split up between the premises, whereas for the additive case connective (&) the context of the conclusion ({{math|Γ}}) is carried whole into both premises.

under a classical interpretation. But now we can explain the basis for the multiplicative/additive distinction

in the rules for the two different versions of conjunction: for the multiplicative connective (⊗),

the context of the conclusion ({{math|Γ, Δ}}) is split up between the premises, whereas

for the additive case connective (&) the context of the conclusion ({{math|Γ}}) is carried whole into both

premises.

===Exponentials===

The exponentials are used to give controlled access to weakening and contraction. Specifically, we add structural rules of weakening and contraction for {{math|?}}'d propositions:{{sfn|Girard|1987|loc=p.25-26, Def.1.21}}

structural rules of weakening and contraction for ?'d propositions:<ref>Girard (1987), p.25-26, Def.1.21</ref>

{| style="margin:auto"

|-

Line 306 ⟶ 303:

|}

|}

and use the following logical rules:

and use the following logical rules, in which {{math|?Γ}} stands for a list of propositions each prefixed with {{math|?}}:

{| style="margin:auto"

|-

Line 329 ⟶ 328:

|}

|}

One might observe that the rules for the exponentials follow a different pattern from the rules for the other connectives,

One might observe that the rules for the exponentials follow a different pattern from the rules for the other connectives, resembling the inference rules governing modalities in sequent calculus formalisations of the [[normal modal logic]] [[S4 (modal logic)|S4]], and that there is no longer such a clear symmetry between the duals {{math|!}} and {{math|?}}. This situation is remedied in alternative

This situation is remedied in alternative presentations of CLL (e.g., the [[Logic of unity|LU]] presentation).

==Remarkable formulas==

Line 379 ⟶ 378:

|}

Linear distributions are fundamental in the proof theory of linear logic. The consequences of this map were first investigated in <ref>J. Robin Cockett and Robert& Seely "Weakly distributive categories" Journal of Pure and Applied Algebra 114(21997) 133-173, 1997</ref> and called a "weak distribution". {{sfn|Cockett|Seely|1997}} In subsequent work it was renamed to "linear distribution" to reflect the fundamental connection to linear logic.

; Other implications :

Line 415 ⟶ 414:

==Encoding classical/intuitionistic logic in linear logic==

Both intuitionistic and classical implication can be recovered from linear implication by inserting exponentials: intuitionistic implication is encoded as {{math|!<VAR>A</VAR> ⊸ <VAR>B</VAR>}}, while classical implication can be encoded as {{math|!?<VAR>A</VAR> ⊸ ?<VAR>B</VAR>}} or {{math|!<VAR>A</VAR> ⊸ ?!<VAR>B</VAR>}} (or a variety of alternative possible translations).<ref>{{sfn|Di Cosmo, Roberto. ''[http://www.dicosmo.org/CourseNotes/LinLog/ The Linear Logic Primer]''. Course notes; chapter 2.</ref>|1996}} The idea is that exponentials allow us to use a formula as many times as we need, which is always possible in classical and intuitionistic logic.

Formally, there exists a translation of formulas of intuitionistic logic to formulas of linear logic in a way that guarantees that the original formula is provable in intuitionistic logic if and only if the translated formula is provable in linear logic. Using the [[Gödel–Gentzen negative translation]], we can thus embed classical [[first-order logic]] into linear first-order logic.

==The resource interpretation==

Line 430 ⟶ 429:

Multiplicative conjunction {{math|(<VAR>A</VAR> ⊗ <VAR>B</VAR>)}} denotes simultaneous occurrence of resources, to be used as the consumer directs. For example, if you buy a stick of gum and a bottle of soft drink, then you are requesting {{math|<VAR>gum</VAR> ⊗ <VAR>drink</VAR>}}. The constant 1 denotes the absence of any resource, and so functions as the unit of ⊗.

Additive conjunction {{math|(<VAR>A</VAR> & <VAR>B</VAR>)}} represents alternative occurrence of resources, the choice of which the consumer controls. If in the vending machine there is a packet of chips, a candy bar, and a can of soft drink, each costing one dollar, then for that price you can buy exactly one of these products. Thus we write {{math|<VAR>$1</VAR> ⊸ (<VAR>candy</VAR> & <VAR>chips</VAR> & <VAR>drink</VAR>)}}. We do ''not'' write {{math|<VAR>$1</VAR> ⊸ (<VAR>candy</VAR> ⊗ <VAR>chips</VAR> ⊗ <VAR>drink</VAR>)}}, which would imply that one dollar suffices for buying all three products together. However, from {{math|(<VAR>$1</VAR> ⊸ (<VAR>candy</VAR> & <VAR>chips</VAR> & <VAR>drink</VAR>)) ⊗ (<VAR>$1</VAR> ⊸ (<VAR>candy</VAR> & <VAR>chips</VAR> & <VAR>drink</VAR>)) ⊗ (<VAR>$1</VAR> ⊸ (<VAR>candy</VAR> & <VAR>chips</VAR> & <VAR>drink</VAR>))}}, we can correctly deduce {{math|<VAR>$3</VAR> ⊸ (<VAR>candy</VAR> ⊗ <VAR>chips</VAR> ⊗ <VAR>drink</VAR>)}}, where {{math|<VAR>$3</VAR> :{{=}} <VAR>$1</VAR> ⊗ <VAR>$1</VAR> ⊗ <VAR>$1</VAR>}}. The unit ⊤ of additive conjunction can be seen as a wastebasket <!--or [[Garbage collection (computer science)|garbage collector]]--> for unneeded resources. For example, we can write {{math|<VAR>$3</VAR> ⊸ (<VAR>candy</VAR> ⊗ ⊤)}} to express that with three dollars you can get a candy bar and some other stuff, without being more specific (for example, chips and a drink, or $2, or $1 and chips, etc.).

Additive disjunction {{math|(<VAR>A</VAR> ⊕ <VAR>B</VAR>)}} represents alternative occurrence of resources, the choice of which the machine controls. For example, suppose the vending machine permits gambling: insert a dollar and the machine may dispense a candy bar, a packet of chips, or a soft drink. We can express this situation as {{math|<VAR>$1</VAR> ⊸ (<VAR>candy</VAR> ⊕ <VAR>chips</VAR> ⊕ <VAR>drink</VAR>)}}. The constant 0 represents a product that cannot be made, and thus serves as the unit of ⊕ (a machine that might produce {{math|<VAR>A</VAR>}} or {{math|0}} is as good as a machine that always produces {{math|<VAR>A</VAR>}} because it will never succeed in producing a 0). So unlike above, we cannot deduce {{math|<VAR>$3</VAR> ⊸ (<VAR>candy</VAR> ⊗ <VAR>chips</VAR> ⊗ <VAR>drink</VAR>)}} from this.

==Other proof systems==

Multiplicative disjunction {{math|(<VAR>A</VAR> ⅋ <VAR>B</VAR>)}} is more difficult to gloss in terms of the resource interpretation, although we can encode back into linear implication, either as {{math|<VAR>A</VAR>^⊥ ⊸ <VAR>B</VAR>}} or {{math|<VAR>B</VAR>^⊥ ⊸ <VAR>A</VAR>}}.

===Proof nets===

== Other proof systems ==

=== Proof nets ===

{{main|Proof net}}

Introduced by [[Jean-Yves Girard]], proof nets have been created to avoid the ''bureaucracy'', that is all the things that make two derivations different in the logical point of view, but not in a "moral" point of view.

Line 475 ⟶ 473:

The goal of proof nets is to make them identical by creating a graphical representation of them.

== Semantics ==

{{Expand section|date=May 2023}}

=== Algebraic semantics ===

{{See also|Quantale}}

==Decidability/complexity of entailment==

The [[entailment]] relation in full CLL is [[Undecidable problem|undecidable]].<ref {{refn|name="Lincoln+92">|For this result and discussion of some of the fragments below, see: {{cite journalharvtxt|first1=Patrick|last1=Lincoln|first2=John|last2=Mitchell|first3=Andre|last3=Scedrov|first4=Natarajan|last4=Shankar|year=1992|title=Decision Problems for Propositional Linear Logic|journal=Annals of Pure and Applied Logic|volume=56|issue=1–3|pages=239–311|doi=10.1016/0168-0072(92)90075-B|doi-access=free}}</ref> }} When considering fragments of

CLL, the decision problem has varying complexity:

* Multiplicative linear logic (MLL): only the multiplicative connectives. MLL entailment is [[NP-complete]], even restricting to [[Horn clauses]] in the purely implicative fragment,<ref>{{Cite conferencesfn| doi = 10.1109/LICS.1992.185533| conference = Seventh Annual IEEE Symposium on Logic in Computer Science, 1992. LICS '92. Proceedings| pages = 200–210| last = Kanovich| first = Max I.| title = Horn programming in linear logic is NP-complete| book-title = Seventh Annual IEEE Symposium on Logic in Computer Science, 1992. LICS '92. Proceedings| date = 1992-06-22| isbn = 0-8186-2735-2}}</ref> or to atom-free formulas.<ref>{{cite journal|first1=Patricksfn|last1=Lincoln|first2=Timothy|last2=Winkler|year=1994|title=Constant-only multiplicative linear logic is NP-complete|journal=Theoretical Computer Science|volume=135|pages=155–169|doi=10.1016/0304-3975(94)00108-1|doi-access=free}}</ref>

* Multiplicative-additive linear logic (MALL): only multiplicatives and additives (i.e., exponential-free). MALL entailment is [[PSPACE-complete]].<ref name="Lincoln+92" />

* Multiplicative-exponential linear logic (MELL): only multiplicatives and exponentials. By reduction from the reachability problem for [[Petri nets]],<ref>{{Cite conferencesfn| conference = Tenth International Conference on Application and Theory of Petri Nets. Proceedings| pages = 174–191| last1 = Gunter| first1 = C. A.| last2 = Gehlot| first2 = V.| year = 1989}}</ref> MELL entailment must be at least [[EXPSPACE|EXPSPACE-hard]], although decidability itself has had the status of a longstanding open problem. In 2015, a proof of decidability was published in the journal ''[[Theoretical Computer Science (journal)|TCSTheoretical Computer Science]]'',<ref>{{Cite journalsfn| doi = 10.1016/j.tcs.2015.06.019| issn = 0304-3975| volume = 597| pages = 1–17| last = Bimbó| first = Katalin|author-link= Katalin Bimbó | title = The decidability of the intensional fragment of classical linear logic| journal = Theoretical Computer Science| date = 2015-09-13| doi-access = free}}</ref> but was later shown to be erroneous.<ref>{{Cite journalsfn| doi = 10.1016/j.tcs.2019.02.022| issn = 0304-3975| volume = 768| pages = 91–98| last = Straßburger| first = Lutz| title = On the decision problem for MELL| journal = Theoretical Computer Science| date = 2019-05-10| doi-access = free}}</ref>

* Affine linear logic (that is linear logic with weakening, an extension rather than a fragment) was shown to be decidable, in 1995.<ref>{{Cite conferencesfn| doi = 10.1109/LICS.1995.523283| citeseerx = 10.1.1.23.9226| conference = Tenth Annual IEEE Symposium on Logic in Computer Science, 1995. LICS '95. Proceedings| pages = 496–504| last = Kopylov| first = A. P.| title = Decidability of linear affine logic| book-title = Tenth Annual IEEE Symposium on Logic in Computer Science, 1995. LICS '95. Proceedings| date = 1995-06-01| isbn = 0-8186-7050-9}}</ref>

==Variants==

Line 504 ⟶ 501:

{{Portal|Philosophy}}

* [[Chu space]]s

* [[Linear type system]], a [[substructural type system]]

* [[LogicComputability of unitylogic]] (LU)

* [[Proof net]]s

* [[Geometry of interaction]]

* [[Game semantics]]

* [[Geometry of interaction]]

* [[Intuitionistic logic]]

* [[ComputabilityLinear logic programming]]

* [[Linear type system]], a [[substructural type system]]

* [[Ludics]]

* [[ChuProof spacenet]]s

* [[Uniqueness type]]

* [[Linear logic programming]]

==Notes==

{{Reflist|2}}

==References==

*{{cite journal|last1=Baez|first1=John|author1-link=John Baez|last2=Stay|first2=Mike|year=2008|title=Physics, Topology, Logic and Computation: A Rosetta Stone|journal=New Structures of Physics|editor=Bob Coecke|editor-link=Bob Coecke|url=http://math.ucr.edu/home/baez/rosetta.pdf}}

{{Reflist}}

*{{Cite journal|last=Bimbó|first=Katalin|author-link=Katalin Bimbó|date=2015-09-13|title=The decidability of the intensional fragment of classical linear logic|journal=Theoretical Computer Science|volume=597|pages=1–17|doi=10.1016/j.tcs.2015.06.019|issn=0304-3975|doi-access=free}}

*{{cite journal|last1=Cockett|first1=J. Robin|author1-link=Robin Cockett|last2=Seely|first2=Robert|year=1997|title=Weakly distributive categories|journal=Journal of Pure and Applied Algebra|volume=114|issue=2|pages=133–173|doi=10.1016/0022-4049(95)00160-3 }}

*{{cite book|last=Di Cosmo|first=Roberto|year=1996|title=The Linear Logic Primer|type=Course notes|chapter=2|url=http://www.dicosmo.org/CourseNotes/LinLog/}}

*{{cite journal|last1=De Paiva|first1=V.|author1-link=Valeria de Paiva|last2=Van Genabith|first2=J.|last3=Ritter|first3=E.|year=1999|title=Dagstuhl Seminar 99341 on Linear Logic and Applications|journal=Drops-Idn/V2/Document/10.4230/Dagsemrep.248|pages=1–21|publisher=Schloss Dagstuhl – Leibniz-Zentrum für Informatik|doi=10.4230/DagSemRep.248|doi-access=free|url=http://www.dagstuhl.de/Reports/99/99341.pdf}}

*{{cite journal|last1=Girard|first1=Jean-Yves|author1-link=Jean-Yves Girard|year=1987|title=Linear logic|journal=Theoretical Computer Science|volume=50|issue=1|pages=1–102|doi=10.1016/0304-3975(87)90045-4|hdl=10338.dmlcz/120513|url=https://girard.perso.math.cnrs.fr/linear.pdf|doi-access=free}}

*{{Cite tech report|last1=Gunter|first1=C. A.|last2=Gehlot|first2=V.|year=1989|title=Nets as Tensor Theories|institution=University of Pennsylvania|number=MS-CIS-89-68|url=http://seclab.illinois.edu/wp-content/uploads/2011/04/GunterG89.pdf}}

*{{Cite conference|last=Kanovich|first=Max I.|date=1992-06-22|title=Horn programming in linear logic is NP-complete|conference=Seventh Annual IEEE Symposium on Logic in Computer Science, 1992. LICS '92. Proceedings|book-title=Seventh Annual IEEE Symposium on Logic in Computer Science, 1992. LICS '92. Proceedings|pages=200–210|doi=10.1109/LICS.1992.185533|isbn=0-8186-2735-2}}

*{{Cite conference|last=Kopylov|first=A. P.|date=1995-06-01|title=Decidability of linear affine logic|conference=Tenth Annual IEEE Symposium on Logic in Computer Science, 1995. LICS '95. Proceedings|book-title=Tenth Annual IEEE Symposium on Logic in Computer Science, 1995. LICS '95. Proceedings|pages=496–504|doi=10.1109/LICS.1995.523283|citeseerx=10.1.1.23.9226|isbn=0-8186-7050-9}}

*{{cite journal|last1=Lincoln|first1=Patrick|last2=Mitchell|first2=John|last3=Scedrov|first3=Andre|last4=Shankar|first4=Natarajan|year=1992|title=Decision Problems for Propositional Linear Logic|journal=Annals of Pure and Applied Logic|volume=56|issue=1–3|pages=239–311|doi=10.1016/0168-0072(92)90075-B|doi-access=free}}

*{{cite journal|last1=Lincoln|first1=Patrick|last2=Winkler|first2=Timothy|year=1994|title=Constant-only multiplicative linear logic is NP-complete|journal=Theoretical Computer Science|volume=135|pages=155–169|doi=10.1016/0304-3975(94)00108-1|doi-access=free}}

*{{Cite journal|last=Straßburger|first=Lutz|date=2019-05-10|title=On the decision problem for MELL|journal=Theoretical Computer Science|volume=768|pages=91–98|doi=10.1016/j.tcs.2019.02.022|issn=0304-3975|doi-access=free}}

==Further reading==

* {{cite web |title=Introduction to Linear Logic |last=Braüner| first=Torben|url=http://www.brics.dk/LS/96/6/BRICS-LS-96-6.pdf |date=December 1996|publisher=Basic Research in Computer Science (BRICS)|volume=LS-96/6|series=BRICS Lecture Series |access-date=2025-05-20}}

* Girard, Jean-Yves. ''[http://girard.perso.math.cnrs.fr/linear.pdf Linear logic]'', Theoretical Computer Science, Vol 50, no 1, pp.&nbsp;1–102, 1987.

* Girard, Jean-Yves, Lafont, Yves, and Taylor, Paul. ''[https://web.archive.org/web/20160704202340/http://www.cs.man.ac.uk/~pt/stable/Proofs+Types.html Proofs and Types]''. Cambridge Press, 1989.

* {{cite book |last1=Di Cosmo |first1=Roberto |last2=Danos |first2=Vincent |year=1992|title=The Linear Logic Primer |url=https://www.dicosmo.org/CourseNotes/LinLog/ }}

* Hoare, C. A. R., 1985. ''Communicating Sequential Processes''. Prentice-Hall International. {{isbn|0-13-153271-5}}

* Lafont, Yves, 1993. ''Introduction to Linear Logic''. Lecture notes from TEMPUS Summer School on ''Algebraic and Categorical Methods in Computer Science'', Brno, Czech Republic.

*{{cite SEP|title=Linear Logic|url-id=logic-linear|date=2023-09-16|edition=Fall 2023|author-last=Di Cosmo|author-first=Roberto|author-last2=Miller|author-first2=Dale |author-link2=Dale Miller (academic)}}

* [[A. S. Troelstra|Troelstra, A.S.]] ''Lectures on Linear Logic''. CSLI (Center for the Study of Language and Information) Lecture Notes No. 29. Stanford, 1992.

* [[A. S. Troelstra]], H. Schwichtenberg (1996). ''Basic Proof Theory''. In series ''Cambridge Tracts in Theoretical Computer Science'', Cambridge University Press, {{isbn|0-521-77911-1}}.

* {{cite book |last1=Girard |first1=Jean-Yves |last2=Lafont |first2=Yves |last3=Taylor |first3=Paul |year=1989 |title=Proofs and Types |publisher=Cambridge University Press |url=http://www.cs.man.ac.uk/~pt/stable/Proofs+Types.html |archive-url=https://web.archive.org/web/20160704202340/http://www.cs.man.ac.uk/~pt/stable/Proofs+Types.html |archive-date=4 July 2016 }}

* Di Cosmo, Roberto, and Danos, Vincent. ''[http://www.dicosmo.org/CourseNotes/LinLog/ The linear logic primer]''.

* [http://www.csl.sri.com/~lincoln/papers/sigact92.ps Introduction to Linear Logic] (Postscript) by [http://www.csl.sri.com/users/lincoln/ Patrick Lincoln]

* {{cite book |last=Hoare |first=C. A. R. |year=1985 |title=Communicating Sequential Processes |publisher=Prentice-Hall International |isbn=0-13-153271-5 }}

* [http://www.brics.dk/LS/96/6/BRICS-LS-96-6.pdf Introduction to Linear Logic] by Torben Brauner

* [http://homepages.inf.ed.ac.uk/wadler/topics/linear-logic.html A taste of linear logic] by Philip Wadler

*{{cite conference | last = Lafont | first = Yves | year = 1993 | title = Introduction to Linear Logic | book-title = TEMPUS Summer School on Algebraic and Categorical Methods in Computer Science | ___location = Brno, Czech Republic | type = Lecture notes}}

* [http://plato.stanford.edu/entries/logic-linear/ Linear Logic] by [https://web.archive.org/web/20060925141642/http://www.pps.jussieu.fr/~dicosmo/index.html.en Roberto Di Cosmo] and [http://www.lix.polytechnique.fr/Labo/Dale.Miller/ Dale Miller]. The Stanford Encyclopedia of Philosophy (Fall 2006 Edition), Edward N. Zalta (ed.).

* [http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/llp.pdf Overview of linear logic programming] by [http://www.lix.polytechnique.fr/Labo/Dale.Miller/ Dale Miller]. In ''Linear Logic in Computer Science'', edited by Ehrhard, Girard, Ruet, and Scott. Cambridge University Press. London Mathematical Society Lecture Notes, Volume 316, 2004.

* {{cite web |title=Introduction to Linear Logic |last=Lincoln |first=Patrick|url=http://www.csl.sri.com/~lincoln/papers/sigact92.ps |format=Postscript }}

* [http://llwiki.ens-lyon.fr/ Linear Logic Wiki]

* {{cite book|last=Miller |first=Dale |year=2004 |chapter=Overview of Linear Logic Programming |title=Linear Logic in Computer Science |editor1-last=Ehrhard |editor2-last=Girard |editor3-last=Ruet |editor4-last=Scott |publisher=Cambridge University Press |series=London Mathematical Society Lecture Notes |volume=316 |url=http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/llp.pdf }}

* {{cite book | last = Troelstra | first = A. S. | author-link = Anne Sjerp Troelstra | year = 1992 | title = Lectures on Linear Logic | publisher = CSLI Publications | ___location = Stanford | series = CSLI Lecture Notes | volume = 29 | isbn = 978-0937073773 }}

* {{cite book |last1=Troelstra |first1=A. S.| author1-link = Anne Sjerp Troelstra|last2=Schwichtenberg |first2=H. |author2-link=Helmut Schwichtenberg|year=2000|orig-year=1996 |title=Basic Proof Theory |series=Cambridge Tracts in Theoretical Computer Science |volume=43|___location=Cambridge |publisher=Cambridge University Press |pages=XII, 417|edition=2nd|isbn=9780521779111|doi=10.1017/CBO9781139168717|oclc=951181823}}

* {{cite web |title=A Taste of Linear Logic |last=Wadler| first=Philip|url=http://homepages.inf.ed.ac.uk/wadler/topics/linear-logic.html }}

==External links==

*{{Commons category-inline}}

* {{Commons category-inline}}

*[http://bach.istc.kobe-u.ac.jp/llprover/ A Linear Logic Prover (llprover)], available for use online, from: Naoyuki Tamura / Dept of CS / Kobe University / Japan

* [http://bach.istc.kobe-u.ac.jp/llprover/ A Linear Logic Prover (llprover)] {{Webarchive|url=https://web.archive.org/web/20160404181455/http://bach.istc.kobe-u.ac.jp/llprover/ |date=2016-04-04 }}, available for use online, from: Naoyuki Tamura / Dept of CS / Kobe University / Japan

* [https://click-and-collect.linear-logic.org/ Click And Collect] interactive linear logic prover, available online

{{Non-classical logic}}