Undecidability of the Transitive Graded Modal Logic with Converse.

We extend the language of the modal logic K4 of transitive frames with two sorts of modalities. In addition to the usual possibility modality (which means that a formula holds in some successor of a given point), we consider graded modalities (a formula holds in at least n successors) and converse graded modalities (a formula holds in at least n predecessors). We show that the resulting logic, GrIK4, is both locally and globally undecidable. The same result is obtained for all logics between GrIK4 and its reflexive companion GrIS4 and for some other modal logics. As a consequence, for the 'unrestricted version' of the description logic SIQ, the problem of concept satisfiability (even with respect to the empty terminology) is undecidable. We also give a survey of results on the local and global decidability, complexity, and the finite model property for fragments of GrIK4.