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——前者采用正则语言路径表达式，后者采用可见下推语言路径表达式的ALC扩展。ALCreg实质上是Fischer与Ladner提出的著名命题动态逻辑的记法变体，而ALCvpl则由Loding和Serre于2007年提出并研究。ALCvpl泛化了ALCreg诸多已知可判定的非正则扩展范式。我们给出了一系列不可判定性结果。首先，证明在ALCvpl中添加看似无害的自指算子(Self operator)后，概念可满足性问题即失去可判定性。其次，论证了扩展了名义词(nominals)的ALCvpl概念可满足性问题不可判定。值得关注的是，该不可判定性证明仅依赖于单一非正则（可见下推）语言r#s# := { r^n s^n | n ∈ N }（固定角色名r,s）。最后，与经典数据库设置形成鲜明对比，我们证明了在仅含ALC-TBoxes的情形下，涉及r#s#非正则原子的查询蕴含关系已经不可判定。