Concrete domains have been introduced in the context of Description Logics to allow references to qualitative and quantitative values. In particular, the class of $\omega$-admissible concrete domains, which includes Allen's interval algebra, the region connection calculus (RCC8), and the rational numbers with ordering and equality, has been shown to yield extensions of $\mathcal{ALC}$ for which concept satisfiability w.r.t. a general TBox is decidable. In this paper, we present an algorithm based on type elimination and use it to show that deciding the consistency of an $\mathcal{ALC}(\mathfrak{D})$ ontology is ExpTime-complete if the concrete domain $\mathfrak{D}$ is $\omega$-admissible and its constraint satisfaction problem is decidable in exponential time. While this allows us to reason with concept and role assertions, we also investigate feature assertions $f(a,c)$ that can specify a constant $c$ as the value of a feature $f$ for an individual $a$. We show that, under conditions satisfied by all known $\omega$-admissible domains, we can add feature assertions without affecting the complexity.

翻译：具体域被引入描述逻辑中，旨在允许对定性和定量值的引用。特别地，$\omega$-可容许具体域类（包括艾伦区间代数、区域连接演算（RCC8）以及具有序和相等关系的有理数）已被证明可以产生 $\mathcal{ALC}$ 的扩展，使得相对于一般 TBox 的概念可满足性是可判定的。本文提出了一种基于类型消除的算法，并用其证明：若具体域 $\mathfrak{D}$ 是 $\omega$-可容许的且其约束满足问题可在指数时间内判定，则判定 $\mathcal{ALC}(\mathfrak{D})$ 本体的可满足性是 ExpTime-完全的。虽然这允许我们处理概念断言和角色断言，但我们也研究了特征断言 $f(a,c)$，它可以将常量 $c$ 指定为个体 $a$ 的特征 $f$ 的值。我们证明，在所有已知 $\omega$-可容许域均满足的条件下，添加特征断言不会影响其复杂性。