We present a KE-tableau-based implementation of a reasoner for a decidable fragment of (stratified) set theory expressing the description logic $\mathcal{DL}\langle \mathsf{4LQS^{R,\!\times}}\rangle(\mathbf{D})$ ($\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$, for short). Our application solves the main TBox and ABox reasoning problems for $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$. In particular, it solves the consistency problem for $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$-knowledge bases represented in set-theoretic terms, and a generalization of the \emph{Conjunctive Query Answering} problem in which conjunctive queries with variables of three sorts are admitted. The reasoner, which extends and optimizes a previous prototype for the consistency checking of $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$-knowledge bases (see \cite{cilc17}), is implemented in \textsf{C++}. It supports $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$-knowledge bases serialized in the OWL/XML format, and it admits also rules expressed in SWRL (Semantic Web Rule Language).

翻译：我们提出了一种基于KE-表方法的推理机实现，用于描述逻辑 $\mathcal{DL}\langle \mathsf{4LQS^{R,\!\times}}\rangle(\mathbf{D})$（简称 $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$）所表达的（分层）集合论的可判定片段。我们的应用解决了 $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$ 的主要TBox和ABox推理问题。具体而言，它解决了以集合论术语表示的 $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$ 知识库的一致性检测问题，以及一种推广的\emph{合取查询回答}问题，该问题允许包含三种类型变量的合取查询。该推理机扩展并优化了先前用于 $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$ 知识库一致性检测的原型系统（参见 \cite{cilc17}），并以 \textsf{C++} 实现。它支持以OWL/XML格式序列化的 $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$ 知识库，并接纳以SWRL（语义网规则语言）表达的规则。