一句话：证明 ALCvpl 加入 Self、nominal 或非正则查询原子后，可满足性与查询蕴涵不可判定。
论文研究在 ALC 上引入非正则路径表达式后，描述逻辑可满足性与查询可判定性的变化。重点考察 ALCreg 与 ALCvpl：前者使用正则路径，是 Fischer-Ladner 命题动态逻辑的记号变体；后者使用 visibly-pushdown 语言，由 Loding 和 Serre 提出，并推广多种已知可判定的非正则扩展。作者围绕单一非正则语言 r#s#={r^n s^n} 证明一系列不可判定性结果：ALCvpl 加入 Self 算子后概念可满足性不可判定；加入 nominals 后亦不可判定；最后，与经典数据库情形相对，证明在 ALC-TBox 下涉及 r#s# 非正则原子的查询蕴涵已不可判定。
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.
@article{paperbot2762,
title = {Exploring Non-Regular Extensions of Propositional Dynamic Logic with Description-Logics Features},
author = {Bartosz Bednarczyk},
journal = {Logical Methods in Computer Science},
volume = {Volume 20, Issue 2},
year = {2024},
doi = {10.46298/lmcs-20(2:7)2024}
}