18
$\begingroup$

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?

Improve this question
$\endgroup$

4 Answers 4

Reset to default
17
$\begingroup$

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."

Improve this answer
$\endgroup$
9
  • 3
    $\begingroup$ 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. $\endgroup$
    – Neel Krishnaswami
    Nov 21, 2011 at 6:09
  • 4
    $\begingroup$ @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.) $\endgroup$
    – Emil Jeřábek
    Nov 21, 2011 at 16:19
  • 1
    $\begingroup$ 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." $\endgroup$
    – Rob Simmons
    Nov 21, 2011 at 18:42
  • 1
    $\begingroup$ @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$? $\endgroup$
    – Rob Simmons
    Nov 21, 2011 at 18:49
  • 1
    $\begingroup$ @Rob Simmons: a satisfying assignment for its negation. $\endgroup$
    – Kaveh
    Nov 22, 2011 at 0:14
11
$\begingroup$

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.

Improve this answer
$\endgroup$
1
  • $\begingroup$ @Kaveh: Misrecollection rather than typo; fixed. I should mention MLL. $\endgroup$
    – Charles Stewart
    Dec 2, 2011 at 11:02
11
$\begingroup$

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
Improve this answer
$\endgroup$
9
$\begingroup$

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

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.