DocumentCode
2144783
Title
Linearizing intuitionistic implication
Author
Lincoln, Patrick ; Scedrov, Andre ; Shankar, Natarajan
Author_Institution
Dept. of Comput. Sci., Stanford Univ., CA, USA
fYear
1991
fDate
15-18 July 1991
Firstpage
51
Lastpage
62
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;
fLanguage
English
Publisher
ieee
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
Type
conf
DOI
10.1109/LICS.1991.151630
Filename
151630
Link To Document