Undecidability of the transitive graded modal logic with converseстатья
Статья опубликована в высокорейтинговом журнале
Информация о цитировании статьи получена из
Scopus
Статья опубликована в журнале из списка Web of Science и/или Scopus
Дата последнего поиска статьи во внешних источниках: 9 ноября 2017 г.
Аннотация:Рассматривается модальный язык, в котором помимо обычной модальности «возможности» (в семантике Крипке означающей «существует последователь, в котором верна данная формула»), имеются градуированные модальности (означающие «существует более n последователей, где верна данная формула») и градуированные обратные модальности (означающие «существует более n предшественников, где верна данная формула»). Доказано, что логика в этом языке класса всех транзитивных (а также транзитивных рефлексивных) шкал Крипке неразрешима. Для основных фрагментов данной логики установлена вычислительная сложность проблем локальной, глобальной и комбинированной выполнимости модальных формул, а также установлено наличие или отсутствие у данных фрагментов локальной, глобальной и комбинированной финитной аппроксимируемости.
===
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 (aformula 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.