×

Modal description logics: Modalizing roles. (English) Zbl 0951.03011

Description logics may be considered as a direct successor of the semantic networks and frames, the traditional knowledge representation tools. They are characterized in the paper as logic-based formalisms intended for representing knowledge about concept hierarchies, supplied with effective reasoning procedures and a Tarski-style declarative semantics.
The paper provides a contribution to the study of concept description languages of high expressive power. A rich multi-dimensional modal description language was designed. The language imposes no restrictions on the use of modal operators. They can be applied to all types of syntactic terms – concepts, roles and formulas. This is the most important feature distinguishing this language from its predecessors. The language contains both local and global object, concept and role names. Multi-dimensional modal description logics of such a great expressivity have never been considered in the literature. The language is intended for representing dynamic and intensional knowledge.
Of course, a price for this expressive power has to be paid. The class of description languages studied in the paper is located near the border between decidable and undecidable. The decidability of some versions of the satisfiability problem is studied in the paper.
A modal description language \({\mathcal A}{\mathcal L}{\mathcal C}_{\mathcal M}\) and its semantics is defined. It is shown that the satisfaction problem for \({\mathcal A}{\mathcal L}{\mathcal C}_{\mathcal M}\)-formulas in models with expanding domains can be reduced to the same problem but in models with constant domains.
It is shown that there is a mosaic-type algorithm checking the satisfiability for this language in (i) arbitrary multimodal frames, (ii) frames with universal accessibility relations, (iii) frames with transitive, symmetric and Euclidean accessibility relations.
The satisfaction problem becomes undecidable if the underlying frames are arbitrary strict linear orders (temporal structures), or the language contains the common knowledge operator for \(n \geq 2\) agents.

MSC:

03B42 Logics of knowledge and belief (including belief change)
68T30 Knowledge representation
03B44 Temporal logic
03B45 Modal logic (including the logic of norms)
68T27 Logic in artificial intelligence
03B70 Logic in computer science
03B25 Decidability of theories and sets of sentences