Intuitionistic propositional logic is polynomial-space complete. (English) Zbl 0411.03049


03F20 Complexity of proofs
03D15 Complexity of computation (including implicit computational complexity)
03F55 Intuitionistic mathematics
03B40 Combinatory logic and lambda calculus
Full Text: DOI Link


[1] Cook, S.A., Feasibly constructive proofs and the propositional calculus, () · Zbl 0357.68061
[2] Cook, S.A.; Reckhow, R.A., On the length of proofs in the propositional calculus, ()
[3] Curry, H.B.; Feys, R., Combinatory logic, Vol. 1, (1968), North-Holland Amsterdam · Zbl 0175.27601
[4] Fitting, M., Intuitionistic logic, modal theory and forcing, (1969), North-Holland Amsterdam · Zbl 0188.32003
[5] Friedman, H., Equality between functionals, () · 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 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, () · 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 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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.