Tree-sequent calculi and decision procedures for intuitionistic modal logics

摘要

In this article we define label-free sequent calculi for the intuitionistic modal logics obtained from the combinations of the axioms T, B, 4 and S. These calculi are based on a multi-contextual sequent structure, called Tree-sequent, which allows us to define such calculi for such intuitionistic modal logics. From the calculi defined for the IK, IT, IB4 and ITB logics, we also provide new decision procedures and alternative syntactic proofs of decidability.