We consider intuitionistic multimodal logics with modalities satisfying axiom K and the axiom of Necessity, as well as collections of axioms for transforming, removing and splitting modalities, specified by a relation between modalities and sequences of modalities. These axioms can be used for systems of knowledge and belief, describing multiple environments of truth and their awareness of each other. We extend Gentzen’s decidable cut-free calculus to accommodate such multimodal systems, using a modal shift operation on contexts to extend the cut elimination proof in a novel way. We then adapt the inverse method to formulate a correct and complete forward proof search for these logics, which can be interpreted in a Fitch-style manner. Proof derivation is streamlined by implementing most derivations using the cut rule. The resulting proof search allows for making multiple queries, building a database of assumptions and their consequences which can be fine-tuned and updated to fit an application.