基于关联解释的术语集MUPS求解方法

Associate interpretation based MUSP calculation in terminologies

本体调试是人工智能中非标准推理任务之一,主要用于找出本体中导致逻辑冲突的解释并进行修改,对于本体工程具有重要意义.结合语法相关性与关联解释,提出一种术语集的极小不可满足子术语集求解方法.语法相关性用于递归扩展不可满足子术语集,从待测术语集中将与不可满足概念语法相关的公理集合加入到不可满足子术语集,一定程度上减少了不相关公理的加入,可以有效减少待测术语集规模.进一步地,将术语集的极小不可满足保持子术语集(minimal unsatisfiability-preserving sub-TBox,MUPS)的求解过程看作是关键公理的查找过程.提出关联解释的定义,并通过构造术语集的关联解释方式确定关键公理.该过程一定程度上减少了推理机调用次数并简化了每次调用用于找出问题时的推理任务.实验部分将各类优化策略应用于黑盒算法并进行了比较.实验结果表明,该方法能够有效提高术语集MUPS求解效率.

Ontology debugging is one of the non-standard reasoning tasks in artificial intelligence,which is very important for the ontology engineering.Ontology debugging is mainly used to find out the interpretations which may cause the logical conflicts in ontologies,and further revise the ontologies to eliminate these conflicts.Technically,calculating minimal unsatisfiability-preserving sub-TBox（MUPS）is the core issue in the ontology debugging.The existing work of MUPS calculation investigates two approaches：one based on modifying the internal of a description logic reasoner（the “glass-box” technology）,and other based on using an unmodified external reasoner（the “black-box” technology）.In our work,one method using syntactic relevance and associate interpretation is proposed to calculate the MUPS for the unsatisfiable classes and terminologies.This method is based on the traditional black-box technology,and further optimizes the expansion and prune procedure in the traditional black-box technology.Firstly,we extend the candidate unsatisfiable sub-TBox by adding the axioms which are structurally relevant with the axioms that contain unsatisfiable classes.By doing this,we can eliminate the irrelevant axioms for the satisfiability to the extent,which may reduce the size of the axioms in terminologies to be checked.Then,the MUPS calculation can be seen as the procedure of seeking the critical axioms in the MUPS.In this procedure,we propose the definition of the associate interpretation,and the associate interpretation is introduced to construct special interpretation which can be used to check the satisfaction of axioms in candidate minimal unsatisfiable sub-TBox.And the number of reasoner call is reduced and further the reasoning problem in each iteration is also simplified.Finally,we realize the algorithm and compare it with the optimizations of the black box algorithm.The experimental results show that the proposed method can effectively improve the efficiency of MUPS calculation in the terminology.