Statman, Richard Intuitionistic propositional logic is polynomial-space complete. (English) Zbl 0411.03049 Theor. Comput. Sci. 9, 67-72 (1979). Page: −5 −4 −3 −2 −1 ±0 +1 +2 +3 +4 +5 Show Scanned Page Cited in 6 ReviewsCited in 68 Documents MSC: 03F20 Complexity of proofs 03D15 Complexity of computation (including implicit computational complexity) 03F55 Intuitionistic mathematics 03B40 Combinatory logic and lambda calculus Keywords:validity in intuitionistic propositional logic; length of derivations; complexity of proofs; Np-completeness; proof theory; typed lambda calculus Citations:Zbl 0411.03047; Zbl 0411.03048; Zbl 0411.03050 × Cite Format Result Cite Review PDF Full Text: DOI Link References: [1] Cook, S. A., Feasibly constructive proofs and the propositional calculus, (Proc. of the 7th Annual Symp. on Theory of Computing (May 1975), A.C.M) · Zbl 0357.68061 [2] Cook, S. A.; Reckhow, R. A., On the length of proofs in the propositional calculus, (Proc. Sixth A.C.M. Symp. on Theory of Computing (May 1974), A.C.M) [3] Curry, H. B.; Feys, R., Combinatory Logic, Vol. 1 (1968), North-Holland: North-Holland Amsterdam · Zbl 0175.27601 [4] Fitting, M., Intuitionistic Logic, Modal Theory and Forcing (1969), North-Holland: North-Holland Amsterdam · Zbl 0188.32003 [5] Friedman, H., Equality between functionals, (Parikh, R., Lecture Notes in Math., 453 (1974), Springer-Verlag: Springer-Verlag Berlin) · Zbl 0311.02040 [6] Howard, W., The formulae-as-types notion of construction (1969), mimeographed [7] Kleene, S. C., Introduction to Mathematics (1952), Van Nostrand: Van Nostrand New York · Zbl 0047.00703 [8] Kreisel, G., A remark on free choice sequences and topological completeness proofs, J. Symbolic Logic, 23, 378 (1958) [9] Kripke, S., Semantical analysis of intuitionistic logic I, (Crossley, J.; Dummett, M., Formal Systems and Recursive Functions (1965), North-Holland: North-Holland Amsterdam) · Zbl 0137.00702 [10] Ladner, R. E., The computational complexity of provability in systems of model propositional logic, SIAM J. Comput., 6, 3 (Sept. 1977) [11] Prawitz, D., Natural Deduction, Stockholm Studies in Philosophy 3 (1965), Almqvist and Wiksell · Zbl 0173.00205 [12] Shoenfield, J. R., Mathematical Logic (1967), Addison-Wesley: Addison-Wesley Reading, MA · Zbl 0155.01102 [13] Statman, R., The typed λ-calculus is not elementary recursive, Theoret. Comput. Sci., 9, 73-81 (1979) · Zbl 0411.03050 [14] Stockmeyer, L. V., The polynomial-time hierarchy, Theoret. Comput. Sci., 3, 1-22 (1976) · Zbl 0353.02024 This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.