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#非正则原子的查询蕴含已不可判定。