Multimodal logics are general modal systems with an arbitrary set of modal operators. In particular, we have studied the class of inclusion and incestual modal logics introduced by Catach which include, among the others, modal and multimodal systems characterized by serial, symmetric, transitive, and Euclidean accessibility relations. These systems can be non-homogeneous (i.e. every modal operator is not restricted to the same system) and can contain some interaction axioms (i.e. each modal operator is not necessarily independent from the others). Multimodal systems are widely used in artificial intelligence for representing knowledge and beliefs together with other attitudes in agent systems like, for instance, goals, intentions and obligations. In particular, they allow agent scenarios to be modelled, in which agents may have different ways of reasoning and of interacting with each other. Furthermore, multimodal logics are well suited for representing dynamic aspects in agent systems and, in particular, to formalize reasoning about actions and time.
For this class of logics we developed a prefixed analytic tableaux calculus. The main feature of the calculus is that it can deal in a uniform way with any multimodal logics in this class [1,5]. In order to achieve this goal, we use a prefixed tableau calculus à la Fitting, where, however, we explicitly represent accessibility relations between worlds by means of a graph, and we use the characterizing axioms of the logic as rewriting rules which create new paths among worlds in the counter-model construction. We proved some (un)decidability results about multimodal logics, and we used the prefixed tableau method to show undecidability of a wide subclass.