18

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?

Anonymous
  • 4,041
  • 19
  • 43

4 Answers4

17

Other resources could be found referenced in Kaustuv Chaudhuri's thesis "The Focused Inverse Method for Linear Logic", and you might be interested in Roy Dyckhoff's "Contraction-Free Sequent Calculi", 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" is a good reference if you want to get technical about words like "easier."

Rob Simmons
  • 2,396
  • 13
  • 24
  • 3
    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 Nov 21 '11 at 06:09
  • 4
    @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 Nov 21 '11 at 16:19
  • 1
    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 Nov 21 '11 at 18:42
  • 1
    @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 Nov 21 '11 at 18:49
  • 1
    @Rob Simmons: a satisfying assignment for its negation. – Kaveh Nov 22 '11 at 00:14
  • Aah. Yes, of course. – Rob Simmons Nov 22 '11 at 02:47
  • @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 Nov 22 '11 at 05:40
  • 1
    @EmilJ: One question, though: if you leave out $\top$, is $A & B$ still ill-behaved? – Neel Krishnaswami Nov 22 '11 at 07:28
  • 1
    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 Nov 23 '11 at 13:57
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 Sylvain Schmitz, Non-Elementary Complexities for Branching VASS, MELL, and Extensions, manuscript, 2014. arXiv:1401.6785 [cs.LO]
  • [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
  • [Sch14] Sylvain Schmitz, Implicational Relevance Logic is 2-ExpTime-complete, manuscript, 2014. arXiv:1402.0705 [cs.LO]
  • [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
  • [Urq84] Alasdair Urquhart, The Undecidability of Entailment and Relevant Implication, Journal of Symbolic Logic 49(4):1059–1073, 1984. doi: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
Sylvain
  • 3,374
  • 26
  • 22
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, 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; this is a good place to look since Miller has done more to develop the idea of proof search as computation as anyone else.

Charles Stewart
  • 4,316
  • 28
  • 45
9

Perhaps Dale Miller's Overview of linear logic programming is a good strarting point?

Andrej Bauer
  • 28,823
  • 1
  • 80
  • 133