[Prev][Next][Index][Thread]
Linearizing Intuitionistic Implication
Date: Wed, 4 Mar 92 16:10:23 EST
To: linear@cs.stanford.edu
Linearizing Intuitionistic Implication
P. Lincoln, A. Scedrov, and N. Shankar
Abstract: An embedding of the implicational propositional intuitionistic
logic (IIL) into the nonmodal fragment of intuitionistic linear logic (IMALL)
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. A preliminary version of this work was reported in LICS '91.
A dvi file of the full paper is available by anonymous ftp by using the
following dialogue:
% ftp ftp.cis.upenn.edu
Name: anonymous
Password: [[enter your email address]]
ftp> cd pub
ftp> binary
ftp> get lss91.dvi
ftp> quit