Title :
Linearizing intuitionistic implication
Author :
Lincoln, Patrick ; Scedrov, Andre ; Shankar, Natarajan
Author_Institution :
Dept. of Comput. Sci., Stanford Univ., CA, USA
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
Keywords :
formal logic; PSPACE-hardness; cut-free proofs; implicational propositional intuitionistic logic; intuitionistic implication; intuitionistic linear logic; nonmodal fragment; proof system; Availability; Calculus; Computer science; Ear; Embedded computing; Helium; Laboratories; Logic; Mathematics;
Conference_Titel :
Logic in Computer Science, 1991. LICS '91., Proceedings of Sixth Annual IEEE Symposium on
Conference_Location :
Amsterdam
Print_ISBN :
0-8186-2230-X
DOI :
10.1109/LICS.1991.151630
