表达性描述逻辑中基数限制与标称推理的复杂性
人工智能
2011-06-02 v1
摘要
我们研究了描述逻辑ALCQ和ALCQI与基于概念基数限制的术语形式体系的组合的复杂性。这些组合可以自然地嵌入到C^2（带计数量词的一阶逻辑的二变量片段）中，从而得到NExpTime的可判定性。我们表明，这种方法为ALCQI带来了最优解，因为带有基数限制的ALCQI与C^2具有相同的复杂性（NExpTime-完全）。相比之下，我们证明对于ALCQ，该问题可以在ExpTime内解决。这一结果是通过将基数限制推理归约为对扩展了标称的ALCQ的一般公理（通常更弱）的术语形式体系的推理而获得的。使用相同的归约，我们证明，对于扩展了标称的ALCQI，一般公理推理是一个NExpTime-完全问题。最后，我们强化了这一结果，并证明带有标称的ALCQI的纯概念可满足性是NExpTime-完全的。没有标称时，已知该问题是PSpace-完全的。
引用
@article{arxiv.1106.0239,
title = {The Complexity of Reasoning with Cardinality Restrictions and Nominals in Expressive Description Logics},
author = {S. Tobies},
journal= {arXiv preprint arXiv:1106.0239},
year = {2011}
}