We present a novel reasoning calculus for the description logic SHOIQ^+---a knowledge representation formalism with applications in areas such as the Semantic Web. Unnecessary nondeterminism and the construction of large models are two primary sources of inefficiency in the tableau-based reasoning calculi used in state-of-the-art reasoners. In order to reduce nondeterminism, we base our calculus on hypertableau and hyperresolution calculi, which we extend with a blocking condition to ensure termination. In order to reduce the size of the constructed models, we introduce anywhere pairwise blocking. We also present an improved nominal introduction rule that ensures termination in the presence of nominals, inverse roles, and number restrictions---a combination of DL constructs that has proven notoriously difficult to handle. Our implementation shows significant performance improvements over state-of-the-art reasoners on several well-known ontologies.

本文提出了一种新的推理演算法，用于描述逻辑SHOIQ+，该逻辑在语义Web等领域具有应用。我们基于超表和超分辨率演算，引入阻塞条件以保证演算终止，并采用任意配对阻塞来减少构造模型的大小。同时，还引入改进的名词引入规则，以确保在存在名词、逆向角色和数量限制等问题时，演算的终止性。我们的实现在多个知名本体上，优于先前的推理器。

描述逻辑的Hypertableau推理