We investigate the impact of non-regular path expressions on the decidability of satisfiability checking and querying in description logics extending ALC. Our primary objects of interest are ALCreg and ALCvpl, the extensions of with path expressions employing, respectively, regular and visibly-pushdown languages. The first one, ALCreg, is a notational variant of the well-known Propositional Dynamic Logic of Fischer and Ladner. The second one, ALCvpl, was introduced and investigated by Loding and Serre in 2007. The logic ALCvpl generalises many known decidable non-regular extensions of ALCreg. We provide a series of undecidability results. First, we show that decidability of the concept satisfiability problem for ALCvpl is lost upon adding the seemingly innocent Self operator. Second, we establish undecidability for the concept satisfiability problem for ALCvpl extended with nominals. Interestingly, our undecidability proof relies only on one single non-regular (visibly-pushdown) language, namely on r#s# := { r^n s^n | n in N } for fixed role names r and s. Finally, in contrast to the classical database setting, we establish undecidability of query entailment for queries involving non-regular atoms from r#s#, already in the case of ALC-TBoxes.

翻译：我们研究了非正则路径表达式对扩展ALC的描述逻辑中可满足性检测与查询判定性的影响。我们的主要研究对象是ALCreg和ALCvpl，这两个扩展分别采用正则语言和可见下推语言的路径表达式。前者ALCreg是Fischer与Ladner经典命题动态逻辑的记法变体，后者ALCvpl由Loding和Serre于2007年提出并研究。ALCvpl泛化了ALCreg的多种已知可判定非正则扩展。我们给出了一系列不可判定性结果：首先，加入看似无害的Self算子后，ALCvpl的概念可满足性问题会丧失可判定性；其次，我们证明扩展了名义词的ALCvpl的概念可满足性问题不可判定。有趣的是，该不可判定性证明仅依赖于单一非正则（可见下推）语言r#s# := { r^n s^n | n ∈ N }（其中r和s为固定角色名）。最后，与经典数据库设置形成鲜明对比的是，我们证明在ALC-TBox场景下，包含r#s#非正则原子的查询蕴含问题已不可判定。