Linearizing intuitionistic implication

Annals of Pure and Applied Logic 60 (2):151-177 (1993)
  Copy   BIBTEX


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 proofs



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

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

The logic of bunched implications.Peter W. O'Hearn & David J. Pym - 1999 - Bulletin of Symbolic Logic 5 (2):215-244.
From if to bi.Samson Abramsky & Jouko Väänänen - 2009 - Synthese 167 (2):207 - 230.


Added to PP

12 (#806,547)

6 months
1 (#454,876)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Natarajan Shankar
International University College

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.

View all 6 citations / Add more citations

References found in this work

Proofs and Types.Jean-Yves Girard - 1989 - Cambridge University Press.
A game semantics for linear logic.Andreas Blass - 1992 - Annals of Pure and Applied Logic 56 (1-3):183-220.
Contraction-free sequent calculi for intuitionistic logic.Roy Dyckhoff - 1992 - Journal of Symbolic Logic 57 (3):795-807.

View all 7 references / Add more references