Modal Tree-Sequents

We develop cut-free calculi of sequents for normal modal logics by using treesequents, which are trees of sequences of formulas. We introduce modal operators corresponding to the ways we move formulas along the branches of such trees, only considering fixed distance movements. Finally, we exhibit syntactic cut-elimination theorems for all the main normal modal logics. Mathematics Subject Classification: 03B45, 03F05.