Annals of Pure and Applied Logic 56 (1-3):239-311 (1992)
AbstractLinear 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
Similar books and articles
Linear logic proof games and optimization.Patrick D. Lincoln, John C. Mitchell & Andre Scedrov - 1996 - Bulletin of Symbolic Logic 2 (3):322-338.
A modal view of linear logic.Simone Martini & Andrea Masini - 1994 - Journal of Symbolic Logic 59 (3):888-899.
The finite model property for knotted extensions of propositional linear logic.C. J. van Alten - 2005 - Journal of Symbolic Logic 70 (1):84-98.
The logic of bunched implications.Peter W. O'Hearn & David J. Pym - 1999 - Bulletin of Symbolic Logic 5 (2):215-244.
Cut-free sequent and tableau systems for propositional diodorean modal logics.Rajeev Goré - 1994 - Studia Logica 53 (3):433 - 457.
Linearizing intuitionistic implication.Patrick Lincoln, Andre Scedrov & Natarajan Shankar - 1993 - Annals of Pure and Applied Logic 60 (2):151-177.
The undecidability of second order linear logic without exponentials.Yves Lafont - 1996 - Journal of Symbolic Logic 61 (2):541-548.
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.
Added to PP
Historical graph of downloads
Citations of this work
Decision problems for propositional linear logic.Patrick Lincoln, John Mitchell, Andre Scedrov & Natarajan Shankar - 1992 - Annals of Pure and Applied Logic 56 (1-3):239-311.
Structural Completeness in Substructural Logics.J. S. Olson, J. G. Raftery & C. J. Van Alten - 2008 - Logic Journal of the IGPL 16 (5):453-495.
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.
References found in this work
The Mathematics of Sentence Structure.Joachim Lambek - 1958 - Journal of Symbolic Logic 65 (3):154-170.
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.