Effective properties of some first order intuitionistic modal logics

Indexed sequent calculi are constructed for first-order intuitionistic moda l logics K, K4, T, S4 with the Barcan axiom as well as for KB, B, and S5, w here the Barcan formula is derivable. Effective properties, namely, admissi bility of the cut rule, Harrop properties, and the interpolation property f or the calculi under consideration are proved using proof-theoretical metho ds. Based on the constructed sequent calculi, computer-aided tableaux-like and resolution calculi can be obtained.