An Introduction to Normal Multimodal Logics Interaction Axioms, Prefixed Tableau Calculus,s.pdf

1An Introduction to Normal Multimodal Logics: Interaction Axioms, Prefixed Tableau Calculus, some [un]Decidability Results, and Applications Matteo Baldoni Dipartimento di Informatica - Universita` degli Studi di Torino C.so Svizzera, 185 - I-10149 Torino (Italy) e-mail: baldoni@di.unito.it URL: http://www.di.unito.it/~baldoni Genova, 3 maggio 2000 An Introduction to Normal Multimodal Logics 2 In the presentation ... ? an introduction to Modal and Multimodal Logics ? a tableau calculus for a wide class of normal multimodal logics (inclusion [Fari?as del Cerro and Penttonen, 1988] and incestual [Catach, 1988] multimodal logics) modular w.r.t. the axiom systems; ? some (un)decidability results for the class of inclusion and incestual multimodal logics; ? an application of inclusion modal logics to logic programming: the logic programming languages NemoLOG and DyLOG. 2Genova, 3 maggio 2000 An Introduction to Normal Multimodal Logics 3 (Mono)Modal Logic Genova, 3 maggio 2000 An Introduction to Normal Multimodal Logics 4 Modal Logics Knowledge Beliefs Actions Dynamic changes Time Modal logics are suitable to deal with reasoning about distributed knowledge 3Genova, 3 maggio 2000 An Introduction to Normal Multimodal Logics 5 The Modal Operator “ “ ? no truth-functional This means that the meaning of this formula does not depend only on the truth-value of its subformulae. This means that ? is not only true but necessarily true, it is true independently from the scenario (or state, world, etc.) It qualifies the truth value of ? Genova, 3 maggio 2000 An Introduction to Normal Multimodal Logics 6 The Modal Operator “ “ ? ? is believed ? is known ? is necessarily true ? is true in any possible scenario ? is always true 4Genova, 3 maggio 2000 An Introduction to Normal Multimodal Logics 7 The Modal Operator “ “: Kripke semantics w ? 1w kw jw nw ? ? ? ?? ?wM , ?iwM , ii wRww :? if and only if ?1, wM ?nwM , ?kwM , M accessibility relation Genova, 3 maggio 2000 An Intro