Paper: Linearizing intuitionistic implication (at LICS 1991)
Authors: Patrick Lincoln Andre Scedrov Natarajan ShankarAbstract
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 Symp. on Logic in Computer Science, {LICS} 1991}, year = 1991, editor = {Giles Kahn}, month = {July}, pages = {51--62}, location = {Amsterdam, The Netherlands}, publisher = {IEEE Computer Society Press} }