A modular sequent calculus labelled with truth values is defined for dealing with a wide class of modal systems. Completeness is established over an algebraic semantics. Some classes of frames are shown to be characterized precisely within the calculus. Normalization and cut elimination results are stated and discussed. This talk reports ongoing joint work with P. Mateus, C. Sernadas and L. Viganò.