描述逻辑SHIN的ABox一致性判定算法

摘要：

为了判定描述逻辑SHIN的ABox一致性，提出了一种Tableau算法。给定TBox T、ABox A和角色层次H，该算法通过预处理将A转换成标准的ABox A′，按照特定的完整策略将一套Tableau规则应用于 A′，直到将它扩展成完整的ABox A″为止。A与T和H一致，当且仅当算法能产生一个完整且无冲突的ABox A″。算法所采用的阻塞机制可以避免Tableau规则的无限次执行，该机制允许一个新个体被在其之前创建的任意新个体直接阻塞，而不仅仅局限于其祖先。通过对算法的可终止性、合理性和完备性进行证明，算法的正确性得以确认。

关键词：支持补集、传递角色、角色层次、反向角色和数量约束的属性语言(SHIN)、ABox一致性判定、Tableau算法、阻塞机制、可终止性、合理性、完备性

分类号：TP301.2(计算技术、计算机技术)

资助基金：国家自然科学基金No.61073191；湖南第一师范学院校级课题No.XYS10N09。

在线出版日期：2013-10-24（万方平台首次上网日期，不代表论文的发表时间）

页数：共8页

页码：55-62