Normal Multimodal Logics: Automatic Deduction and Logic Programming Extension

In this thesis we work on normal multimodal logics, that are general modal systems with an arbitrary set of normal modal operators, focusing on the class of inclusion modal logics. This class of logics, first introduced by Fariñas del Cerro and Penttonen, includes some well-known non-homogeneous multimodal systems characterized by interaction axioms of the form [t1][t2]... [tn]ϕ ⊃ [s1][s2]... [sm]ϕ, that we call inclusion axioms. The thesis is organized in two part. In the first part the class of inclusion modal logics is deeply studied by introducing the the syntax, the possible-worlds semantics, and the axiomatization. Afterwards, we define a proof theory based on an analytic tableau calculus. The main feature of the calculus is that it can deal in a uniform way with any multimodal logics in the considered class. 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 path among worlds in the counter-model construction. Some (un)decidability results for this class of logic are given. Moreover, the tableau metho