[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