Cut-free tableau calculi for some propositional normal modal logics

We give sound and complete tableau and sequent calculi for the prepositional normal modal logics S4.04, K4B and G⁰(these logics are the smallest normal modal logics containing K and the schemata A A, A A and A ( A); A A and AA; A A and ((A A) A) A resp.) with the following properties: the calculi for S4.04 and G⁰are cut-free and have the interpolation property, the calculus for K4B contains a restricted version of the cut-rule, the so-called analytical cut-rule.In addition we show that G⁰is not compact (and therefore not canonical), and we proof with the tableau-method that G⁰is characterised by the class of all finite, (transitive) trees of degenerate or simple clusters of worlds; therefore G⁰is decidable and also characterised by the class of all frames for G⁰.Research supported by Fonds zur Förderung der wissenschaftlichen Forschung, project number P8495-PHY.Presented by W. Rautenberg