Labelled Modal Sequents

In this paper we present a new labelled sequent calculus for modal logic. The proof method works with a more ``liberal'' modal language which allows inferential steps where different formulas refer to different labels without moving to a particular world and there computing if the consequence holds. World-paths can be composed, decomposed and manipulated through unification algorithms and formulas in different worlds can be compared even if they are sub-formulas which do not depend directly on the main connective. Accordingly, such a sequent system can provide a general definition of modal consequence relation. Finally, we briefly sketch a proof of the soundness and completeness results