| Title:
|
On sequent calculi for intuitionistic propositional logic (English) |
| Author:
|
Švejdar, Vítězslav |
| Language:
|
English |
| Journal:
|
Commentationes Mathematicae Universitatis Carolinae |
| ISSN:
|
0010-2628 (print) |
| ISSN:
|
1213-7243 (online) |
| Volume:
|
47 |
| Issue:
|
1 |
| Year:
|
2006 |
| Pages:
|
159-173 |
| . |
| Category:
|
math |
| . |
| 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. (English) |
| Keyword:
|
intuitionistic logic |
| Keyword:
|
polynomial-space |
| Keyword:
|
sequent calculus |
| Keyword:
|
Kripke semantics |
| MSC:
|
03B20 |
| MSC:
|
03B35 |
| MSC:
|
03F05 |
| MSC:
|
03F20 |
| idZBL:
|
Zbl 1138.03008 |
| idMR:
|
MR2223976 |
| . |
| Date available:
|
2009-05-05T16:56:29Z |
| Last updated:
|
2012-04-30 |
| Stable URL:
|
http://hdl.handle.net/10338.dmlcz/119583 |
| . |
| Reference:
|
[1] Buss S., Pudlák P.: On the computational content of intuitionistic propositional proofs.Ann. Pure Appl. Logic 109 49-64 (2001). Zbl 1009.03027, MR 1835237 |
| Reference:
|
[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 |
| Reference:
|
[3] Dershowitz N., Manna Z.: Proving termination with multiset orderings.Comm. ACM 22 465-476 (1979). Zbl 0431.68016, MR 0540043 |
| Reference:
|
[4] Dyckhoff R.: Contraction-free sequent calculi for intuitionistic logic.J. Symbolic Logic 57 795-807 (1992). Zbl 0761.03004, MR 1187448 |
| Reference:
|
[5] Hudelmaier J.: An $O(n\log n)$-space decision procedure for intuitionistic propositional logic.J. Logic Comput. 3 1 63-75 (1993). Zbl 0788.03010, MR 1240404 |
| Reference:
|
[6] Kleene S.C.: Introduction to Metamathematics.D. van Nostrand, New York, 1952. Zbl 0875.03002, MR 0051790 |
| Reference:
|
[7] Ladner R.: The computational complexity of provability in systems of modal logic.SIAM J. Comput. 6 3 467-480 (1977). MR 0450027 |
| Reference:
|
[8] Papadimitriou C.H.: Computational Complexity.Addison-Wesley, Reading, MA, 1994. Zbl 0833.68049, MR 1251285 |
| Reference:
|
[9] Statman R.: Intuitionistic propositional logic is polynomial-space complete.Theoretical Comput. Sci. 9 67-72 (1979). Zbl 0411.03049, MR 0535124 |
| Reference:
|
[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}. Zbl 1025.03030, MR 2015096 |
| Reference:
|
[11] Takeuti G.: Proof Theory.North-Holland, Amsterdam, 1975. Zbl 0681.03039, MR 0882549 |
| Reference:
|
[12] Troelstra A.S., Schwichtenberg H.: Basic Proof Theory.Cambridge University Press, Cambridge, 1996. Zbl 0957.03053, MR 1409368 |
| . |
