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 Farinas 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 a 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 method is extended in order to deal with a wide class of normal multimodal logics that includes the ones characterized by serial, symmetric, and Euclidean accessibility relations. In the second part, we propose the logic programming language NemoLOG. This language extends the Horn clauses logic allowing free occurrences of universal modal operators in front of goals, in front of clauses, and in front of clause heads. The considered multi-modal systems are the ones of the class of inclusion modal logics. The aim of our proposal is not only to extend logic languages in order to perform epistemic reasoning and reasoning about actions but especially to provide tools for software engineering (e.g. modularity and inheritance among classes) retaining a declarative interpretation of the programs. A proof theory is developed for NemoLOG and the soundness and completeness with respect to the model theory are shown by a fixed point construction.