Modular sequent calculi for classical modal logics

This paper develops sequent calculi for several classical modal logics. Utilizing a polymodal translation of the standard modal language, we are able to establish a base system for the minimal classical modal logic E from which we generate extensions (to include M, C, and N) in a modular manner. Our systems admit contraction and cut admissibility, and allow a systematic proof-search procedure of formal derivations