Page 1

Displaying 1 – 4 of 4

Showing per page

On sequent calculi for intuitionistic propositional logic

Vítězslav Švejdar (2006)

Commentationes Mathematicae Universitatis Carolinae

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.

Currently displaying 1 – 4 of 4

Page 1