Article
Full entry |
PDF
(0.3 MB)
Feedback
PDF
(0.3 MB)
Feedback
Keywords:
intuitionistic logic; polynomial-space; sequent calculus; Kripke semantics
intuitionistic logic; polynomial-space; sequent calculus; Kripke semantics
Summary:
The well-known Dyckoff's 1992 calculus/procedure for intuitionistic propositional logic is considered and analyzed. It is shown that the calculus is Kripke complete and the procedure in fact works in polynomial space. Then a multi-conclusion intuitionistic calculus is introduced, obtained by adding one new rule to known calculi. A simple proof of Kripke completeness and polynomial-space decidability of this calculus is given. An upper bound on the depth of a Kripke counter-model is obtained.
References:
[1] Buss S., Pudlák P.: On the computational content of intuitionistic propositional proofs. Ann. Pure Appl. Logic 109 49-64 (2001). MR 1835237 | Zbl 1009.03027
[2] van Dalen D.: Intuitionistic logic. in: Handbook of Philosophical Logic, D. Gabbay and F. Guenthner, Eds., no. 164-167 in Synthese Library, Chapter III.4, pp.225-340, Kluwer, Dordrecht, 1986. Zbl 1002.03053
[3] Dershowitz N., Manna Z.: Proving termination with multiset orderings. Comm. ACM 22 465-476 (1979). MR 0540043 | Zbl 0431.68016
[4] Dyckhoff R.: Contraction-free sequent calculi for intuitionistic logic. J. Symbolic Logic 57 795-807 (1992). MR 1187448 | Zbl 0761.03004
[5] Hudelmaier J.: An $O(n\log n)$-space decision procedure for intuitionistic propositional logic. J. Logic Comput. 3 1 63-75 (1993). MR 1240404 | Zbl 0788.03010
[6] Kleene S.C.: Introduction to Metamathematics. D. van Nostrand, New York, 1952. MR 0051790 | Zbl 0875.03002
[7] Ladner R.: The computational complexity of provability in systems of modal logic. SIAM J. Comput. 6 3 467-480 (1977). MR 0450027
[8] Papadimitriou C.H.: Computational Complexity. Addison-Wesley, Reading, MA, 1994. MR 1251285 | Zbl 0833.68049
[9] Statman R.: Intuitionistic propositional logic is polynomial-space complete. Theoretical Comput. Sci. 9 67-72 (1979). MR 0535124 | Zbl 0411.03049
[10] Švejdar V.: On the polynomial-space completeness of intuitionistic propositional logic. Arch. Math. Logic 42 7 (2003), 711-716; { http://dx.doi.org/10.1007/s00153-003-0179-x} MR 2015096 | Zbl 1025.03030
[11] Takeuti G.: Proof Theory. North-Holland, Amsterdam, 1975. MR 0882549 | Zbl 0681.03039
[12] Troelstra A.S., Schwichtenberg H.: Basic Proof Theory. Cambridge University Press, Cambridge, 1996. MR 1409368 | Zbl 0957.03053
Search
Partner of
