<p>No, it is only ever harder.</p>

<p>Just as the decision problem for intuitionistic propositional logic is harder than of classical propositional logic, so to is linear propositional logic harder still.  With either exponentials (which don't lack contraction) or various flavours of noncommutative connective, the logic becomes undecidable and even the weakling classical MALL is PSPACE complete.  By contrast, the decision problem for classical propositional logic is co-NP complete, and for intuitionistic propositional logic, PSPACE complete.  (Offhand, I don't know the complexity of intuitionistic MALL.)</p>

<p>I recommend Pat Lincoln's exposition in section 6 of his <a href="http://www.csl.sri.com/users/lincoln/papers/sigact92.pdf">Linear logic</a>, SIGACT News 1992.  We have learned a bit more since then, that is, we have results for a large family of linear logics, but the basic picture is there.</p>

<p>In a certain way, this is what makes proof search for linear logic interesting, since hardness of the decision problem makes space for more interesting notions of computation, and linear logic is hard in so many different ways.  Andrej pointed to Dale Miller's <a href="http://www.lix.polytechnique.fr/~dale/papers/llp.pdf">An Overview of Linear Logic Programming</a>; this is a good place to look since Miller has done more to develop the idea of <em>proof search as computation</em> as anyone else.</p>

CC BY-SA 3.0
2011-12-02T11:02:50.983Z
@Kaveh: Misrecollection rather than typo; fixed.  I should mention MLL.
Charles Stewart
CC BY-SA 3.0
2011-11-29T21:59:02.060Z
2011-12-02T11:01:58.377Z
2011-12-02T11:01:58.377Z
Charles Stewart
<p>Assuming that the complexity of the provability problem would satisfy you, the landscape of complexities of substructural logics with and without contraction is somewhat complex.  I'll try to survey here what is known for propositional linear logic and propositional logic.  The short answer is that contraction sometimes helps (e.g. LLC is decidable, while LL isn't), and sometimes doesn't (e.g. MALL is PSPACE-complete, MALLC is ACKERMANN-complete).</p>

<h3>Propositional Logics</h3>

<ul>
<li>CL: classical logic</li>
<li>IL: intuitionistic logic</li>
<li>LL: linear logic, fragments MLL (multiplicative), MELL (multiplicative exponential), MALL (multiplicative additive)</li>
<li>LLW: affine logic, i.e. LL with weakening, same fragments as above</li>
<li>LLC: contractive linear logic, i.e. LL with contraction, same fragments as above</li>
<li>R: relevance logic; differs from MALLC by distributivity rules, implicational fragment R$_\to$, conjunctive-implicational fragment R$_{\to,\wedge}$</li>
</ul>

<h3>Complexity of Provability</h3>

<ul>
<li>NP-complete: MLL [Kan91]</li>
<li>co-NP-complete: CL</li>
<li>PSPACE-complete: IL [Sta79], MALL [Lin92]</li>
<li>2EXP-complete: R$_\to$, IMLLC, IMELLC [Sch14]</li>
<li>TOWER-complete: MELLW, LLW [Laz14]</li>
<li>ACKERMANN-complete: R$_{\to,\wedge}$ [Urq99], MALLC, LLC [Laz14]</li>
<li>$\Sigma_1^0$-complete: LL [Lin92], R [Urq84]</li>
</ul>

<p>Some of the main open questions here are whether MELL is decidable, and what is the complexity of the implicational fragment T$_\to$ of ticket logic (a variant of R).</p>

<h3>References</h3>

<ul>
<li>[Kan91] Max Kanovich, <em>The multiplicative fragment of linear logic is NP-complete</em>, Research Report X-91-13, Institute for Language, Logic, and Information, 1991.</li>
<li>[Laz14] Ranko Lazić and Sylvain Schmitz, <em>Non-Elementary Complexities for Branching VASS, MELL, and Extensions</em>, manuscript, 2014. <a href="http://arxiv.org/abs/1401.6785" rel="nofollow">arXiv:1401.6785 [cs.LO]</a></li>
<li>[Lin92] Patrick Lincoln, John Mitchell, Andre Scedrov, and Natarajan Shankar, <em>Decision problems for propositional linear logic</em>, Annals of Pure and Applied Logic 56(1&ndash;3):239&ndash;311, 1992.  <a href="http://dx.doi.org/10.1016/0168-0072(92)90075-B" rel="nofollow">10.1016/0168-0072(92)90075-B</a></li>
<li>[Sch14] Sylvain Schmitz, <em>Implicational Relevance Logic is 2-ExpTime-complete</em>, manuscript, 2014.  <a href="http://arxiv.org/abs/1402.0705" rel="nofollow">arXiv:1402.0705 [cs.LO]</a></li>
<li>[Sta79] Richard Statman, <em>Intuitionistic propositional logic is polynomial-space complete</em>, Theoretical Computer Science 9(1):67&ndash;72, 1979.  <a href="http://dx.doi.org/10.1016/0304-3975(79)90006-9" rel="nofollow">doi:10.1016/0304-3975(79)90006-9</a></li>
<li>[Urq84] Alasdair Urquhart, <em>The Undecidability of Entailment and Relevant Implication</em>, Journal of Symbolic Logic 49(4):1059&ndash;1073, 1984. <a href="http://dx.doi.org/10.2307/2274261" rel="nofollow">doi:10.2307/2274261</a></li>
<li>[Urq99] Alasdair Urquhart, <em>The Complexity of Decision Procedures In Relevance Logic II</em>, Journal of Symbolic Logic 64(4):1774&ndash;1802, 1999. <a href="http://dx.doi.org/10.2307/2586811" rel="nofollow">10.2307/2586811</a></li>
</ul>

CC BY-SA 3.0
2014-01-28T11:05:05.427Z
2014-02-05T03:18:51.830Z
2014-02-05T03:18:51.830Z
Sylvain
<p>Perhaps Dale Miller's <a href="http://www.lix.polytechnique.fr/~dale/papers/llp.pdf">Overview of linear logic programming</a> is a good strarting point?</p>

CC BY-SA 3.0
2011-11-19T08:43:43.243Z
2011-11-19T08:43:43.243Z
Andrej Bauer
<p>Other resources could be found referenced in Kaustuv Chaudhuri's thesis "<a href="http://www.lix.polytechnique.fr/~kaustuv/papers/chaudhuri06thesis.pdf">The Focused Inverse Method for Linear Logic</a>", and you might be interested in Roy Dyckhoff's "<a href="http://www.jstor.org/pss/2275431">Contraction-Free Sequent Calculi</a>", which is about contraction but not about linear logic.</p>

<p>There are opportunities for efficient proof search in linear logic, but I don't think current work indicates that it's easier than proof search in non-substructural logic. The problem is that if you want to prove $C \vdash(A \otimes B)$ in linear logic, you have an extra question that you don't have in normal proof search: is $C$ used to prove $A$ or is $C$ used to prove $B$? In practice, this "resource nondeterminism" is a big problem in performing proof search in linear logic.</p>

<p>Per the comments, Lincoln et al's 1990 "<a href="http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=89588&amp;tag=1">Decision problems for propositional linear logic</a>" is a good reference if you want to get technical about words like "easier."</p>

CC BY-SA 3.0
2011-11-21T06:09:53.127Z
Isn't proof search in LL harder than IL? ISTR, classical propositional logic is NP-complete, intuitionistic propositional logic is PSPACE-complete, and intuitionistic linear logic (with $!A$) is undecidable.
Neel Krishnaswami
CC BY-SA 3.0
2011-11-21T16:19:14.313Z
@Neel: Exponentials are a device to sneak contraction back in. Also, the additive connectives internally behave as if they have contraction, so you don’t want these either. What you are left with is MLL, which is indeed NP-complete (unlike classical logic, which is not NP-complete as you said, but coNP-complete). In particular, every MLL-tautology has a polynomial-size proof. However, this proof is not easy to find deterministically, as Rob explains (which is a good thing, as we want NP not to be in subexponential time.)
Emil Jeřábek
CC BY-SA 3.0
2011-11-21T18:42:24.000Z
You both serve point out that I was speaking very informally about why linear logic is "not easier" - in a formal sense MALL proof search is harder, and full linear logic proof search is harder still. Most, if not all, of the results ya'll are referring to are from Lincoln et al in the 1990 paper "Decision Problems for Propositional Linear Logic."
Rob Simmons
CC BY-SA 3.0
2011-11-21T18:49:34.030Z
@Emil - I hadn't ever latched on to that interesting difference between MLL and classical logic. MLL is in NP because it's witnesses must be small... but classical propositional sequent proofs need not be polynomial-sized (and I guess can't, in general, be $\it cut$ down to size). What's the polynomial witness for there's-no classical-sequent-proof-of-$A$?
Rob Simmons
CC BY-SA 3.0
2011-11-22T00:14:42.467Z
@Rob Simmons: a satisfying assignment for its negation.
Kaveh
CC BY-SA 3.0
2011-11-22T02:47:03.600Z
Aah. Yes, of course.
Rob Simmons
CC BY-SA 3.0
2011-11-22T05:40:35.890Z
@EmilJ: yes, of course you're correct about classical logic. SAT finds an existential witness, and proving a theorem requires universality, which is co-NP.
Neel Krishnaswami
CC BY-SA 3.0
2011-11-22T07:28:30.580Z
@EmilJ: One question, though: if you leave out $\top$, is $A \& B$ still ill-behaved?
Neel Krishnaswami
CC BY-SA 3.0
2011-11-23T13:57:48.157Z
I guess my comment was too sloppy. Usually, the additive fragment is only considered together with the multiplicative connectives (MALL). If you take *only* the additive connectives (including constants), then the resulting calculus is unary (all derivable sequents are of the form $A\vdash B$), and then it’s easy to see that each derivable sequent has a poly-size proof, and there is a poly-time proof search procedure. I suppose this also works in the presence of negation.
Emil Jeřábek
CC BY-SA 3.0
2011-11-19T23:50:23.810Z
2011-11-21T18:52:05.523Z
2011-11-21T18:52:05.523Z
Rob Simmons
<p>Is automatic theorem proving and proof searching easier in linear and other propositional substructural logics which lack contraction? </p>

<p>Where can I read more about automatic theorem proving in these logics and the role of contraction in proof search?</p>

<reference-request><lo.logic><survey><automated-theorem-proving><linear-logic>
Automated theorem proving in linear logic
Anonymous
# Automated theorem proving in linear logic

(Asked by: username_0 on 2011-11-19)

Is automatic theorem proving and proof searching easier in linear and other propositional substructural logics which lack contraction?

Where can I read more about automatic theorem proving in these logics and the role of contraction in proof search?

**Tags:** reference-request, lo.logic, survey, automated-theorem-proving, linear-logic


---

## 4 answers

### Answer by username_4 on 2011-11-19. Score: 17 | Accepted answer

Other resources could be found referenced in Kaustuv Chaudhuri's thesis "[The Focused Inverse Method for Linear Logic](http://www.lix.polytechnique.fr/~kaustuv/papers/chaudhuri06thesis.pdf)", and you might be interested in Roy Dyckhoff's "[Contraction-Free Sequent Calculi](http://www.jstor.org/pss/2275431)", which is about contraction but not about linear logic.

There are opportunities for efficient proof search in linear logic, but I don't think current work indicates that it's easier than proof search in non-substructural logic. The problem is that if you want to prove $C \vdash(A \otimes B)$ in linear logic, you have an extra question that you don't have in normal proof search: is $C$ used to prove $A$ or is $C$ used to prove $B$? In practice, this "resource nondeterminism" is a big problem in performing proof search in linear logic.

Per the comments, Lincoln et al's 1990 "[Decision problems for propositional linear logic](http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=89588&tag=1)" is a good reference if you want to get technical about words like "easier."

> **Comments:**
> **username_5**: Isn't proof search in LL harder than IL? ISTR, classical propositional logic is NP-complete, intuitionistic propositional logic is PSPACE-complete, and intuitionistic linear logic (with $!A$) is undecidable.  
> **username_6**: @Neel: Exponentials are a device to sneak contraction back in. Also, the additive connectives internally behave as if they have contraction, so you don’t want these either. What you are left with is MLL, which is indeed NP-complete (unlike classical logic, which is not NP-complete as you said, but coNP-complete). In particular, every MLL-tautology has a polynomial-size proof. However, this proof is not easy to find deterministically, as Rob explains (which is a good thing, as we want NP not to be in subexponential time.)  
> **username_4**: You both serve point out that I was speaking very informally about why linear logic is "not easier" - in a formal sense MALL proof search is harder, and full linear logic proof search is harder still. Most, if not all, of the results ya'll are referring to are from Lincoln et al in the 1990 paper "Decision Problems for Propositional Linear Logic."  
> **username_4**: @Emil - I hadn't ever latched on to that interesting difference between MLL and classical logic. MLL is in NP because it's witnesses must be small... but classical propositional sequent proofs need not be polynomial-sized (and I guess can't, in general, be $\it cut$ down to size). What's the polynomial witness for there's-no classical-sequent-proof-of-$A$?  
> **username_7**: @username_4: a satisfying assignment for its negation.  
> **username_4**: Aah. Yes, of course.  
> **username_5**: @EmilJ: yes, of course you're correct about classical logic. SAT finds an existential witness, and proving a theorem requires universality, which is co-NP.  
> **username_5**: @EmilJ: One question, though: if you leave out $\top$, is $A \& B$ still ill-behaved?  
> **username_6**: I guess my comment was too sloppy. Usually, the additive fragment is only considered together with the multiplicative connectives (MALL). If you take *only* the additive connectives (including constants), then the resulting calculus is unary (all derivable sequents are of the form $A\vdash B$), and then it’s easy to see that each derivable sequent has a poly-size proof, and there is a poly-time proof search procedure. I suppose this also works in the presence of negation.  

---

### Answer by username_1 on 2011-11-29. Score: 11

No, it is only ever harder.

Just as the decision problem for intuitionistic propositional logic is harder than of classical propositional logic, so to is linear propositional logic harder still. With either exponentials (which don't lack contraction) or various flavours of noncommutative connective, the logic becomes undecidable and even the weakling classical MALL is PSPACE complete. By contrast, the decision problem for classical propositional logic is co-NP complete, and for intuitionistic propositional logic, PSPACE complete. (Offhand, I don't know the complexity of intuitionistic MALL.)

I recommend Pat Lincoln's exposition in section 6 of his [Linear logic](http://www.csl.sri.com/users/lincoln/papers/sigact92.pdf), SIGACT News 1992. We have learned a bit more since then, that is, we have results for a large family of linear logics, but the basic picture is there.

In a certain way, this is what makes proof search for linear logic interesting, since hardness of the decision problem makes space for more interesting notions of computation, and linear logic is hard in so many different ways. Andrej pointed to Dale Miller's [An Overview of Linear Logic Programming](http://www.lix.polytechnique.fr/~dale/papers/llp.pdf); this is a good place to look since Miller has done more to develop the idea of *proof search as computation* as anyone else.

> **Comments:**
> **username_1**: @username_7: Misrecollection rather than typo; fixed.  I should mention MLL.  

---

### Answer by username_2 on 2014-01-28. Score: 11

Assuming that the complexity of the provability problem would satisfy you, the landscape of complexities of substructural logics with and without contraction is somewhat complex. I'll try to survey here what is known for propositional linear logic and propositional logic. The short answer is that contraction sometimes helps (e.g. LLC is decidable, while LL isn't), and sometimes doesn't (e.g. MALL is PSPACE-complete, MALLC is ACKERMANN-complete).

### Propositional Logics

* CL: classical logic
* IL: intuitionistic logic
* LL: linear logic, fragments MLL (multiplicative), MELL (multiplicative exponential), MALL (multiplicative additive)
* LLW: affine logic, i.e. LL with weakening, same fragments as above
* LLC: contractive linear logic, i.e. LL with contraction, same fragments as above
* R: relevance logic; differs from MALLC by distributivity rules, implicational fragment R$\_\to$, conjunctive-implicational fragment R$\_{\to,\wedge}$

### Complexity of Provability

* NP-complete: MLL [Kan91]
* co-NP-complete: CL
* PSPACE-complete: IL [Sta79], MALL [Lin92]
* 2EXP-complete: R$\_\to$, IMLLC, IMELLC [Sch14]
* TOWER-complete: MELLW, LLW [Laz14]
* ACKERMANN-complete: R$\_{\to,\wedge}$ [Urq99], MALLC, LLC [Laz14]
* $\Sigma\_1^0$-complete: LL [Lin92], R [Urq84]

Some of the main open questions here are whether MELL is decidable, and what is the complexity of the implicational fragment T$\_\to$ of ticket logic (a variant of R).

### References

* [Kan91] Max Kanovich, *The multiplicative fragment of linear logic is NP-complete*, Research Report X-91-13, Institute for Language, Logic, and Information, 1991.
* [Laz14] Ranko Lazić and username_2 Schmitz, *Non-Elementary Complexities for Branching VASS, MELL, and Extensions*, manuscript, 2014. [arXiv:1401.6785 [cs.LO]](http://arxiv.org/abs/1401.6785)
* [Lin92] Patrick Lincoln, John Mitchell, Andre Scedrov, and Natarajan Shankar, *Decision problems for propositional linear logic*, Annals of Pure and Applied Logic 56(1–3):239–311, 1992. [10.1016/0168-0072(92)90075-B](http://dx.doi.org/10.1016/0168-0072(92)90075-B)
* [Sch14] username_2 Schmitz, *Implicational Relevance Logic is 2-ExpTime-complete*, manuscript, 2014. [arXiv:1402.0705 [cs.LO]](http://arxiv.org/abs/1402.0705)
* [Sta79] Richard Statman, *Intuitionistic propositional logic is polynomial-space complete*, Theoretical Computer Science 9(1):67–72, 1979. [doi:10.1016/0304-3975(79)90006-9](http://dx.doi.org/10.1016/0304-3975(79)90006-9)
* [Urq84] Alasdair Urquhart, *The Undecidability of Entailment and Relevant Implication*, Journal of Symbolic Logic 49(4):1059–1073, 1984. [doi:10.2307/2274261](http://dx.doi.org/10.2307/2274261)
* [Urq99] Alasdair Urquhart, *The Complexity of Decision Procedures In Relevance Logic II*, Journal of Symbolic Logic 64(4):1774–1802, 1999. [10.2307/2586811](http://dx.doi.org/10.2307/2586811)


---

### Answer by username_3 on 2011-11-19. Score: 9

Perhaps Dale Miller's [Overview of linear logic programming](http://www.lix.polytechnique.fr/~dale/papers/llp.pdf) is a good strarting point?


---

