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

Natarajan Shankar
International University College
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
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1016/0168-0072(92)90075-b
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 70,265
Through your library

References found in this work BETA

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

Citations of this work BETA

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.

View all 37 citations / Add more citations

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 index

Total views
20 ( #558,064 of 2,507,714 )

Recent downloads (6 months)
4 ( #169,849 of 2,507,714 )

How can I increase my downloads?


My notes