Linearizing intuitionistic implication
Annals of Pure and Applied Logic 60 (2):151-177 (1993)
Abstract
An embedding of the implicational propositional intuitionistic logic into the nonmodal fragment of intuitionistic linear logic is given. The embedding preserves cut-free proofs in a proof system that is a variant of IIL. The embedding is efficient and provides an alternative proof of the PSPACE-hardness of IMALL. It exploits several proof-theoretic properties of intuitionistic implication that analyze the use of resources in IIL proofsAuthor's Profile
DOI
10.1016/0168-0072(93)90041-b
My notes
Similar books and articles
A weak intuitionistic propositional logic with purely constructive implication.Mitsuhiro Okada - 1987 - Studia Logica 46 (4):371 - 382.
The logic of bunched implications.Peter W. O'Hearn & David J. Pym - 1999 - Bulletin of Symbolic Logic 5 (2):215-244.
Expressing Second-order Sentences in Intuitionistic Dependence Logic.Fan Yang - 2013 - Studia Logica 101 (2):323-342.
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.
The pleasures of anticipation: Enriching intuitionistic logic. [REVIEW]Lloyd Humberstone - 2001 - Journal of Philosophical Logic 30 (5):395-438.
Natural Semantics: Why Natural Deduction is Intuitionistic.James W. Garson - 2001 - Theoria 67 (2):114-139.
Grafting modalities onto substructural implication systems.Marcello D'agostino, Dov M. Gabbay & Alessandra Russo - 1997 - Studia Logica 59 (1):65-102.
Combining Derivations and Refutations for Cut-free Completeness in Bi-intuitionistic Logic.Linda Postniece - unknown
Structuralist logic: Implications, inferences, and consequences. [REVIEW]Arnold Koslow - 2007 - Logica Universalis 1 (1):167-181.
Contrariety and Subcontrariety: The Anatomy of Negation (with Special Reference to an Example of J.-Y. Béziau).Lloyd Humberstone - 2005 - Theoria 71 (3):241-262.
A Finite Hilbert‐Style Axiomatization of the Implication‐Less Fragment of the Intuitionistic Propositional Calculus.Jordi Rebagliato & Ventura Verdú - 1994 - Mathematical Logic Quarterly 40 (1):61-68.
Intuitionistic mathematics does not needex falso quodlibet.Neil Tennant - 1994 - Topoi 13 (2):127-133.
Disjunction and existence under implication in elementary intuitionistic formalisms.S. C. Kleene - 1962 - Journal of Symbolic Logic 27 (1):11-18.
An addendum: Disjunction and existence under implication in elementary intuitionistic formalisms.S. C. Kleene - 1963 - Journal of Symbolic Logic 28 (2):154-156.
Analytics
Added to PP
2014-01-16
Downloads
12 (#806,547)
6 months
1 (#454,876)
2014-01-16
Downloads
12 (#806,547)
6 months
1 (#454,876)
Historical graph of downloads
Author's Profile
Citations of this work
Linearizing intuitionistic implication.Patrick Lincoln, Andre Scedrov & Natarajan Shankar - 1993 - Annals of Pure and Applied Logic 60 (2):151-177.
The complexity of Horn fragments of Linear Logic.Max I. Kanovich - 1994 - Annals of Pure and Applied Logic 69 (2-3):195-241.
Linear logic as a logic of computations.Max I. Kanovich - 1994 - Annals of Pure and Applied Logic 67 (1-3):183-212.
A modal view of linear logic.Simone Martini & Andrea Masini - 1994 - Journal of Symbolic Logic 59 (3):888-899.
Petri nets, Horn programs, Linear Logic and vector games.Max I. Kanovich - 1995 - Annals of Pure and Applied Logic 75 (1-2):107-135.
References found in this work
A game semantics for linear logic.Andreas Blass - 1992 - Annals of Pure and Applied Logic 56 (1-3):183-220.
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.
Contraction-free sequent calculi for intuitionistic logic.Roy Dyckhoff - 1992 - Journal of Symbolic Logic 57 (3):795-807.
Uniform proofs as a foundation for logic programming.Dale Miller, Gopalan Nadathur, Frank Pfenning & Andre Scedrov - 1991 - Annals of Pure and Applied Logic 51 (1-2):125-157.
