Linearizing intuitionistic implication
- 10 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
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
This publication has 7 references indexed in Scilit:
- Decision problems for propositional linear logicPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Contraction-free sequent calculi for intuitionistic logicThe Journal of Symbolic Logic, 1992
- Uniform proofs as a foundation for logic programmingAnnals of Pure and Applied Logic, 1991
- Gentzen-type systems and resolution rules part I propositional logicLecture Notes in Computer Science, 1990
- Linear logicTheoretical Computer Science, 1987
- A decidable fragment of predicate calculusTheoretical Computer Science, 1984
- Intuitionistic propositional logic is polynomial-space completeTheoretical Computer Science, 1979