On the Undecidability of Description and Dynamic Logics with Recursion and Counting

The evolution of Description Logics (DLs) and Propositional Dynamic Logics produced a hierar­ chy of decidable logics with multiple maximal el­ ements. It would be desirable to combine different maximal logics into one super-logic, but then in­ ference may turn out to be undecidable. Then it is important to characterize the decidability thresh­ old for these logics. In this perspective, an interest­ ing open question pointed out by Sattler and Vardi [Sattler and Vardi, 1999] is whether inference in a hybrid μ-calculus with restricted forms of graded modalities is decidable, and which complexity class it belongs to. In this paper we prove that this calcu­ lus and the corresponding are un­ decidable. Second, we prove undecidability results for logics that support both a transitive closure op­ erator over roles and number restrictions.

• Type: Conference
• Year: 2003
• Where: IJCAI
• Authors: Piero A. Bonatti
• Keywords: Decidable Logics, IJCAI 2003, IJCAI 2007, Logics, Propositional Dynamic Logics