Giada Coppi


D. Galmiche and Y. Salhi. Tree-sequent calculi and decision procedures for intuitionistic modal logics. Journal of Logic and Computation, 28(5): 967-989, 2018. PDF

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 5. 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.