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-TBox场景下，包含r#s#非正则原子的查询蕴含问题已不可判定。