ИСТИНА

This research is motivated by applications of modal logics to knowledge representation, in particular, by the research in description logics (DLs). In order to formulate the results, we need to specify three things. First, the language we consider is the extension of the multimodal language by the so called graded modalities, which mean that a formula holds in at least (or at most) n successors of a given world. Secondly, the classes of Kripke frames we are interested in are determined by two kinds of constraints: (1) some accessibility relation is transitive; (2) some accessibility relation is contained in some other one. A finite collection of such constraints is called an RBox (a term used in the DL research community). Thirdly, the reasoning problem. Typically, the main problem investigated in modal logic is that of validity, or dually, local satisfiability of formulas: whether a given formula holds in some world of some Kripke model (from a given class). On the contrary, in DLs a crucial role is played by the problem of global satisfiability: whether a given formula holds in all worlds of some Kripke model (from a given class). We present results on (un)decidability of the global satisfiability problem of graded modal formulas in the classes of frames determined by various RBoxes. In our setting, the decidability of the problem depends only on the choice of an RBox. We also discuss some related decidability and complexity results in modal logic, show their relationship to the research in DL and, finally, list some open problems. (Joint work with Yevgeny Kazakov, Oxford University.)