$\mathcal{ALC}$ 中基于 $\omega$-可接受具体域的推理精确复杂性（扩展版）

具体域已在描述逻辑中引入，以允许对定性和定量值进行引用。特别是，$\omega$-可接受具体域的类，包括 Allen 的区间代数、区域连接计算（RCC8），以及带排序和相等性的有理数，已被证明可产生$\mathcal{ALC}$的扩展，其对一般 TBox 下的概念可满足性是可判定的。本文中，我们提出一种基于类型消除的算法，用以证明若具体域 $\mathfrak{D}$ 为 $\omega$-可接受且其约束满足问题可在指数时间内判定，则决定 $\mathcal{ALC}(\mathfrak{D})$ 本体一致性是 ExpTime-complete。虽然这使我们能够对概念和角色断言进行推理，我们也研究了特征断言 $f(a,c)$，其可指定特征 $f$ 对于个体 $a$ 的值为常量 $c$。我们证明了在所有已知 $\omega$-可接受域都满足的条件下，我们可以添加特征断言而不影响复杂性。