基于集合论片段的Web本体表示与推理

在本文中，我们利用可计算集合论(Computable Set Theory)的结果作为表示和推理语义Web描述逻辑与规则语言的方法。具体而言，我们引入描述逻辑 $\mathcal{DL}\langle 4LQS^R\rangle(\D)$——它允许诸如包含公理左右侧的最小/最大基数构造、角色链公理以及数据类型等特征——与支撑Web本体语言OWL的描述逻辑 $\mathcal{SROIQ}(\D)$ 相比，它表现出相当强的表达能力。然后我们证明，$\mathcal{DL}\langle 4LQS^R\rangle(\D)$ 知识库的一致性问题可通过合适的翻译过程归约为集合论的分层片段 $4LQS^R$ 的可满足性问题而判定，该片段涉及四种类型的变量和受限的量化形式。我们还证明了，在适当的非严格约束下，$\mathcal{DL}\langle 4LQS^R\rangle(\D)$ 知识库的一致性问题为 \textbf{NP} 完全。最后，我们给出了属于语义Web规则语言(SWRL)的规则的 $4LQS^R$-翻译。