We present a KE-tableau-based procedure for the main TBox and ABox reasoning tasks for the description logic $\mathcal{DL}\langle \mathsf{4LQS^{R,\!\times}}\rangle(\mathbf{D})$, in short $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$. The logic $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$, representable in the decidable multi-sorted quantified set-theoretic fragment $\mathsf{4LQS^R}$, combines the high scalability and efficiency of rule languages such as the Semantic Web Rule Language (SWRL) with the expressivity of description logics. Our algorithm is based on a variant of the KE-tableau system for sets of universally quantified clauses, where the KE-elimination rule is generalized in such a way as to incorporate the $\gamma$-rule. The novel system, called KE$^\gamma$-tableau, turns out to be an improvement of the system introduced in \cite{RR2017} and of standard first-order KE-tableau \cite{dagostino94}. Suitable benchmark test sets executed on C++ implementations of the three mentioned systems show that the performances of the KE$^\gamma$-tableau-based reasoner are often up to about 400% better than the ones of the other two systems. This a first step towards the construction of efficient reasoners for expressive OWL ontologies based on fragments of computable set-theory.

翻译：本文针对描述逻辑$\mathcal{DL}\langle \mathsf{4LQS^{R,\!\times}}\rangle(\mathbf{D})$（简记为$\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$）提出了基于KE-演算的TBox与ABox主要推理任务程序。该逻辑$\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$可在可判定的多类量化集合论片段$\mathsf{4LQS^R}$中表示，兼具语义网规则语言（SWRL）等规则语言的高可扩展性与高效性，以及描述逻辑的表达能力。我们的算法基于面向全称量化子句集的KE-演算变体，通过推广KE消解规则使其融入$\gamma$-规则。这一新型系统（称为KE$^\gamma$-演算）既改进了文献\cite{RR2017}提出的系统，也优于标准一阶KE-演算\cite{dagostino94}。针对上述三种系统的C++实现所执行的基准测试集表明，基于KE$^\gamma$-演算的推理器性能通常比其他两个系统提升约400%。这是基于可计算集合论片段构建表达性OWL本体高效推理器的初步探索。