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的多种已知可判定非正则扩展。我们给出了一系列不可判定性结果。首先，证明在ALCvpl中添加看似无害的Self算子会导致概念可满足性问题丧失可判定性。其次，建立扩展了名义词后的ALCvpl概念可满足性问题的不可判定性。有趣的是，我们的不可判定性证明仅依赖于单一非正则（可见下推）语言，即针对固定角色名r与s的r#s# := {r^n s^n | n∈N}。最后，与经典数据库设置形成对比，我们证明在ALC-TBoxes情况下，涉及r#s#中非正则原子的查询蕴含即不可判定。