表达性描述逻辑中基数约束和名形推理的复杂性
The Complexity of Reasoning with Cardinality Restrictions and Nominals in Expressive Description Logics
摘要：
我们研究的复杂性相结合的描述逻辑ALCQ和ALCQI的术语形式主义的基础上基数限制的概念。这些组合可以自然地嵌入到C^2中，C^2是谓词逻辑的两个变量片段，具有计数量词，这在NExpTime中产生了可判定性。我们表明，这种方法导致ALCQI的最佳解决方案，因为具有基数限制的ALCQI具有与C^2（NExpTime-complete）相同的复杂性。相反，我们表明，对于ALCQ，问题可以在ExpTime中解决。这一结果是通过减少基数限制推理推理与（一般较弱）术语形式主义的一般公理ALCQ扩展与名词。使用相同的减少，我们表明，对于ALCQI与名义的扩展，推理与一般公理是一个NExpTime完全的问题。最后，我们锐化这一结果，并表明纯概念的ALCQI与名词可满足性是NExpTime-complete。如果没有名词，这个问题被认为是PSpace完全的。
英文摘要：
We study the complexity of the combination of the Description Logics ALCQ and ALCQI with a terminological formalism based on cardinality restrictions on concepts. These combinations can naturally be embedded into C^2, the two variable fragment of predicate logic with counting quantifiers, which yields decidability in NExpTime. We show that this approach leads to an optimal solution for ALCQI, as ALCQI with cardinality restrictions has the same complexity as C^2 (NExpTime-complete). In contrast, we show that for ALCQ, the problem can be solved in ExpTime. This result is obtained by a reduction of reasoning with cardinality restrictions to reasoning with the (in general weaker) terminological formalism of general axioms for ALCQ extended with nominals. Using the same reduction, we show that, for the extension of ALCQI with nominals, reasoning with general axioms is a NExpTime-complete problem. Finally, we sharpen this result and show that pure concept satisfiability for ALCQI with nominals is NExpTime-complete. Without nominals, this problem is known to be PSpace-complete.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
