A Tableau Calculus for Multimodal Logics and some (Un)Decidability Results

In this paper we present a prefixed analytic tableau calculus for a class of normal multimodal logics and we present some results about decidability and undecidability of this class. The class is characterized by axioms of the form [t1 ] . . . [tn ]φ ⊃ [s1 ] . . . [sm ]φ, called inclusion axioms, where the ti ’s and sj ’s are constants. This class of logics, called grammar logics, was introduced for the first time by Fari ̃ as del Cerro and Pentton nen to simulate the behaviour of grammars in modal logics, and includes some well-known modal systems. The prefixed tableau method is used to prove the undecidability of modal systems based on unrestricted, context sensitive, and context free grammars. Moreover, we show that the class of modal logics, based on right-regular grammars, are decidable by means of the filtration methods, by defining an extension of the Fischer-Ladner closure.