【摘要】 公理定位能够挖掘描述逻辑中可解释的缺陷,并为逻辑蕴含结果寻找隐藏的理由,因此在描述逻辑研究中引起了广泛的关注.平衡描述逻辑表达能力和推理机求解效率问题一直是公理定位研究的重点内容.基于一种后继式判定算法,从白盒和黑盒两个角度将其用于公理定位.白盒方法利用修正的后继式规则(即定位规则)来追踪推理的具体过程,并引入定位公式的概念建立子句的布尔公式标签与逻辑蕴含的所有极小公理集之间的对应关系.黑盒方法则直接调用基于未修正的后继式规则的推理机,并进一步利用碰集树方法求得逻辑蕴含的所有理由.最后,基于这样的两种面向强表达描述逻辑本体的公理定位算法设计推理工具,从理论和实验两方面验证其可行性,并与已有的推理工具比较求解性能.更多还原

【Abstract】 Axiom pinpointing has attracted extensive interest for description logics due to its effect of exploring explicable defects in the ontology and searching hidden justifications for the logic consequence. Balancing the expressive power of description logics and the solving efficiency of reasoners has always been the focus of axiom pinpointing research. This study, from both glass-box and black-box perspectives proposed a consequence-based method to computing justifications. The glass-box method uses modified reasoning rules to trace the specific process of inference, and introduces the concept of pinpointing formula to establish the correspondence between the label of Boolean formula and all the minimal axioms sets. The black-box method directly calls the inference engine based on the unmodified reasoning rules, and further uses the HST to compute all justifications for the inference. Two reasoning tools have been designed based on the two axiom pinpointing algorithms for expressive description logics ontologies. Its feasibility is verified theoretically and experimentally, and its solving efficiency is compared with that of existing axiom pinpointing tools.更多还原