Description logics (DL) are a family of formal languages for representing and reasoning about structured knowledge in terms of concepts and their relationships. A central reasoning problem in DL is concept subsumption. Although this problem has been widely studied, important open problems remain for certain logics. The expressive power of DLs depends on the constructors available for building complex concepts. In this work, we investigate subsumption in the restricted logic $\mathcal{FL}_{\bot \mathit{reg}}$ and its related fragments $\mathcal{FL}_\mathit{reg}$, $\mathcal{FL}_\bot$, and $\mathcal{FL}_0$. These logics support value restrictions over role names, where the subscript $\bot$ denotes the presence of the empty concept and ${reg}$ denotes the use of regular expressions over roles. None of these logics includes concept negation. We show that deciding subsumption between two concept descriptions in $\mathcal{FL}_{\bot \mathit{reg}}$ and $\mathcal{FL}_\mathit{reg}$ is PSpace-complete. When subsumption is considered with respect to a TBox (i.e., a set of axioms), the complexity increases to ExpTime-complete. Our results are obtained via a novel reduction to parity pushdown games.

翻译：描述逻辑（DL）是一族形式语言，用于以概念及其关系的形式表示和推理结构化知识。DL 中的一个核心推理问题是概念包含。尽管该问题已被广泛研究，但特定逻辑仍存在重要的开放问题。DL 的表达能力取决于用于构建复杂概念的构造子。本文研究了受限逻辑 $\mathcal{FL}_{\bot \mathit{reg}}$ 及其相关片段 $\mathcal{FL}_\mathit{reg}$、$\mathcal{FL}_\bot$ 和 $\mathcal{FL}_0$ 中的包含关系。这些逻辑支持角色名上的值限制，其中下标 $\bot$ 表示存在空概念，${reg}$ 表示使用角色上的正则表达式。这些逻辑均不包含概念否定。我们证明，在 $\mathcal{FL}_{\bot \mathit{reg}}$ 和 $\mathcal{FL}_\mathit{reg}$ 中判定两个概念描述之间的包含关系是 PSpace 完全的。当考虑相对于 TBox（即一组公理）的包含关系时，复杂度上升至 ExpTime 完全。我们的结果通过一种到奇偶下推游戏的新颖归约获得。