一种用于ABox推理服务的集合论方法（扩展版）
A set-theoretical approach for ABox reasoning services (Extended Version)
AI总结：
本文通过将描述逻辑DL_D^{4,×}的ABox推理服务归约到集合论片段FLQS^R的可满足性问题，提出HOCQA框架和基于KE的答案集计算演算，证明其可判定性并支持SWRL等规则语言。
摘要：
本文考虑描述逻辑 $\mathcal{DL}\langle \mathsf{4LQS^{R,\\!\times}}\rangle(\mathbf{D})$（简记为 $\mathcal{DL}_{\mathbf{D}}^{4,\\!\times}$）中最常见的ABox推理服务，并通过归约到集合论片段 \flqsr 的可满足性问题来证明其可判定性。描述逻辑 $\mathcal{DL}_{\mathbf{D}}^{4,\\!\times}$ 具有很强的表达能力，因为它支持多种概念构造子、角色构造子以及数据类型，从而能够表示诸如SWRL等基于规则的语言。可判定性结果通过定义合取查询应答问题的一种推广形式——称为HOCQA（高阶合取查询应答）——而获得，该形式可实例化为最广泛的ABox推理任务。我们还提出了一种基于 \ke 的方法，用于从 $\mathcal{DL}_{\mathbf{D}}^{4,\\!\times}$ 知识库和高阶 $\mathcal{DL}_{\mathbf{D}}^{4,\\!\times}$ 合取查询中计算答案集，从而为若干众所周知的ABox推理任务提供推理手段。我们的演算扩展了先前为CQA问题引入的基于 \ke 的判定过程。
英文摘要：
In this paper we consider the most common ABox reasoning services for the description logic $\mathcal{DL}\langle \mathsf{4LQS^{R,\!\times}}\rangle(\mathbf{D})$ ($\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$, for short) and prove their decidability via a reduction to the satisfiability problem for the set-theoretic fragment \flqsr. The description logic $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$ is very expressive, as it admits various concept and role constructs, and data types, that allow one to represent rule-based languages such as SWRL. Decidability results are achieved by defining a generalization of the conjunctive query answering problem, called HOCQA (Higher Order Conjunctive Query Answering), that can be instantiated to the most wide\-spread ABox reasoning tasks. We also present a \ke\space based procedure for calculating the answer set from $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$ knowledge bases and higher order $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$ conjunctive queries, thus providing means for reasoning on several well-known ABox reasoning tasks. Our calculus extends a previously introduced \ke\space based decision procedure for the CQA problem.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
