Paper: Linearizing intuitionistic implication (at LICS 1991)

Authors: Patrick Lincoln Andre Scedrov Natarajan 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

BibTeX

  @InProceedings{LincolnScedrovShank-Linearizingintuitio,
    author = 	 {Patrick Lincoln and Andre Scedrov and Natarajan Shankar},
    title = 	 {Linearizing intuitionistic implication},
    booktitle =  {Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science (LICS 1991)},
    year =	 {1991},
    month =	 {July}, 
    pages =      {51--62},
    location =   {Amsterdam, The Netherlands}, 
    publisher =	 {IEEE Computer Society Press}
  }