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

摘要：

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

关键词：描述逻辑SHIF、ABox一致性判定、Tableau算法、阻塞机制、正确性

所属期刊栏目：30

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

资助基金：国家自然科学基金资助项目61073191;湖南第一师范学院校级课题项目XYS10N09

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

页数：共6页

页码：423-428