Intuitionistic propositional logic is polynomial-space complete

DOI10.1016/0304-3975(79)90006-9zbMath0411.03049WikidataQ56224787 ScholiaQ56224787MaRDI QIDQ1259589

Richard Statman

Publication date: 1979

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/2027.42/23534

zbMATH Keywords

proof theory; complexity of proofs; typed lambda calculus; Np-completeness; length of derivations; validity in intuitionistic propositional logic

Mathematics Subject Classification ID

03D15: Complexity of computation (including implicit computational complexity)

03F55: Intuitionistic mathematics

03B40: Combinatory logic and lambda calculus

03F20: Complexity of proofs

Related Items

Graph decompositions and tree automata in reasoning with uncertainty, Complexity of interpolation and related problems in positive calculi, The emptiness problem for intersection types, Substitutions of \(\Sigma_1^0\)-sentences: Explorations between intuitionistic propositional logic and intuitionistic arithmetic, Unification under a mixed prefix, Linearizing intuitionistic implication, The typed lambda-calculus is not elementary recursive, Infiniteness of \(\text{proof}(\alpha)\) is polynomial-space complete, The complexity of the disjunction and existential properties in intuitionistic logic, The complexity of Horn fragments of linear logic, Complexity of some problems in positive and related calculi, On the polynomial-space completeness of intuitionistic propositional logic, Proof finding algorithms for implicational logics, Partial up an down logic

Cites Work

• The polynomial-time hierarchy
• The typed lambda-calculus is not elementary recursive
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item