Decision problems for propositional linear logic

Annals of Pure and Applied Logic 56 (1-3):239-311 (1992)
  Copy   BIBTEX


Linear logic, introduced by Girard, is a refinement of classical logic with a natural, intrinsic accounting of resources. This accounting is made possible by removing the ‘structural’ rules of contraction and weakening, adding a modal operator and adding finer versions of the propositional connectives. Linear logic has fundamental logical interest and applications to computer science, particularly to Petri nets, concurrency, storage allocation, garbage collection and the control structure of logic programs. In addition, there is a direct correspondence between polynomial-time computation and proof normalization in a bounded form of linear logic. In this paper we show that unlike most other propositional logics, full propositional linear logic is undecidable. Further, we prove that without the modal storage operator, which indicates unboundedness of resources, the decision problem becomes PSPACE-complete. We also establish membership in NP for the multiplicative fragment, NP-completeness for the multiplicative fragment extended with unrestricted weakening, and undecidability for fragments of noncommutative propositional linear logic



    Upload a copy of this work     Papers currently archived: 76,199

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

A modal view of linear logic.Simone Martini & Andrea Masini - 1994 - Journal of Symbolic Logic 59 (3):888-899.
The logic of bunched implications.Peter W. O'Hearn & David J. Pym - 1999 - Bulletin of Symbolic Logic 5 (2):215-244.
Linearizing intuitionistic implication.Patrick Lincoln, Andre Scedrov & Natarajan Shankar - 1993 - Annals of Pure and Applied Logic 60 (2):151-177.
Isomorphic formulae in classical propositional logic.Kosta Došen & Zoran Petrić - 2012 - Mathematical Logic Quarterly 58 (1):5-17.
A survey of propositional realizability logic.Valery Plisko - 2009 - Bulletin of Symbolic Logic 15 (1):1-42.
The Propositional Logic of Elementary Tasks.Giorgi Japaridze - 2000 - Notre Dame Journal of Formal Logic 41 (2):171-183.
A parallel game semantics for Linear Logic.Stefano Baratella & Stefano Berardi - 1997 - Archive for Mathematical Logic 36 (3):189-217.
The decision problem of provability logic with only one atom.Vítězslav Švejdar - 2003 - Archive for Mathematical Logic 42 (8):763-768.
A generalised model of judgment aggregation.Franz Dietrich - 2007 - Social Choice and Welfare 4 (28):529-565.


Added to PP

22 (#521,808)

6 months
1 (#448,894)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Natarajan Shankar
International University College

Citations of this work

Proof Theory of Finite-valued Logics.Richard Zach - 1993 - Dissertation, Technische Universität Wien
Multimodal linguistic inference.Michael Moortgat - 1996 - Journal of Logic, Language and Information 5 (3-4):349-385.
Proof complexity of substructural logics.Raheleh Jalali - 2021 - Annals of Pure and Applied Logic 172 (7):102972.

View all 40 citations / Add more citations

References found in this work

The Mathematics of Sentence Structure.Joachim Lambek - 1958 - Journal of Symbolic Logic 65 (3):154-170.
Proofs and Types.Jean-Yves Girard - 1989 - Cambridge University Press.
The Semantics and Proof Theory of Linear Logic.Arnon Avron - 1988 - Theoretical Computer Science 57 (2):161-184.
Quantales and (noncommutative) linear logic.David N. Yetter - 1990 - Journal of Symbolic Logic 55 (1):41-64.
The structure of multiplicatives.Vincent Danos & Laurent Regnier - 1989 - Archive for Mathematical Logic 28 (3):181-203.

View all 11 references / Add more references