Geodesic
On sequent calculi for intuitionistic propositional logic
Commentationes Mathematicae Universitatis Carolinae, Tome 47 (2006) no. 1, pp. 159-173

Voir la notice de l'article provenant de la source Czech Digital Mathematics Library

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.
Classification : 03B20, 03B35, 03F05, 03F20
Keywords: intuitionistic logic; polynomial-space; sequent calculus; Kripke semantics 
@article{CMUC_2006__47_1_a14,
     author = {\v{S}vejdar, V{\'\i}t\v{e}zslav},
     title = {On sequent calculi for intuitionistic propositional logic},
     journal = {Commentationes Mathematicae Universitatis Carolinae},
     pages = {159--173},
     publisher = {mathdoc},
     volume = {47},
     number = {1},
     year = {2006},
     mrnumber = {2223976},
     zbl = {1138.03008},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/CMUC_2006__47_1_a14/}
}
TY  - JOUR
AU  - Švejdar, Vítězslav
TI  - On sequent calculi for intuitionistic propositional logic
JO  - Commentationes Mathematicae Universitatis Carolinae
PY  - 2006
SP  - 159
EP  - 173
VL  - 47
IS  - 1
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/CMUC_2006__47_1_a14/
LA  - en
ID  - CMUC_2006__47_1_a14
ER  - 
%0 Journal Article
%A Švejdar, Vítězslav
%T On sequent calculi for intuitionistic propositional logic
%J Commentationes Mathematicae Universitatis Carolinae
%D 2006
%P 159-173
%V 47
%N 1
%I mathdoc
%U http://geodesic.mathdoc.fr/item/CMUC_2006__47_1_a14/
%G en
%F CMUC_2006__47_1_a14
Švejdar, Vítězslav. On sequent calculi for intuitionistic propositional logic. Commentationes Mathematicae Universitatis Carolinae, Tome 47 (2006) no. 1, pp. 159-173. http://geodesic.mathdoc.fr/item/CMUC_2006__47_1_a14/