Abstract

We present tableau systems and sequent calculi for the intuitionistic analoguesIK, ID, IT, IKB, IKDB, IB, IK4, IKD4, IS4, IKB4, IK5, IKD5, IK45, IKD45 andIS5 of the normal classical modal logics. We provide soundness and completeness theorems with respect to the models of intuitionistic logic enriched by a modal accessibility relation, as proposed by G. Fischer Servi. We then show the disjunction property forIK, ID, IT, IKB, IKDB, IB, IK4, IKD4, IS4, IKB4, IK5, IK45 andIS5. We also investigate the relationship of these logics with some other intuitionistic modal logics proposed in the literature.