Affiliations: Institut für Informatik, Universität Leipzig, Augustus- Platz 10-11, 04109 Leipzig, Germany. e-mail: wolter@informatik.uni-leipzig.de | School of Computer Studies, University of Leeds, Leeds LS2 9JT, England. e-mail: mz@scs.leeds.ac.uk
Note: [] Address for correspondence: Institut für Informatik, Universität Leipzig, Augustus-Platz 10-11, 04109 Leipzig, Germany
Note: [] Address for correspondence: School of Computer Studies, University of Leeds, Leeds LS2 9JT, England
Abstract: We construct a new concept description language intended for representing dynamic and intensional knowledge. The most important feature distinguishing this language from its predecessors in the literature is that it allows applications of modal operators to all kinds of syntactic terms: concepts, roles and formulas. Moreover, the language may contain both local (i.e., state-dependent) and global (i.e., state-independent) concepts, roles and objects. All this provides us with the most complete and natural means for reflecting the dynamic and intensional behaviour of application domains. We construct a satisfiability checking (mosaic-type) algorithm for this language (based on 𝒜ℒ𝒞) in (i) arbitrary multimodal frames, (ii) frames with universal accessibility relations (for knowledge) and (iii) frames with transitive, symmetric and euclidean relations (for beliefs). On the other hand, it is shown that the satisfaction problem becomes undecidable if the underlying frames are arbitrary strict linear orders, 〈$\mathbb{N}$, <〉, or the language contains the common knowledge operator for n ≥ 2 agents.
