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

ABox consistency decision algorithm for description logic SHIN

作　　者：彭立[1] 杨恒伏[1] 

机构地区：[1]湖南第一师范学院信息科学与工程系,长沙410205

出　　处：《计算机工程与应用》2013年第20期55-62,共8页Computer Engineering and Applications

基　　金：国家自然科学基金(No.61073191);湖南第一师范学院校级课题(No.XYS10N09)

摘　　要：为了判定描述逻辑SHIN的ABox一致性,提出了一种Tableau算法。给定TBox T、ABox A和角色层次H,该算法通过预处理将A转换成标准的ABox A′,按照特定的完整策略将一套Tableau规则应用于A′,直到将它扩展成完整的ABox A″为止。A与T和H一致,当且仅当算法能产生一个完整且无冲突的ABox A″。算法所采用的阻塞机制可以避免Tableau规则的无限次执行,该机制允许一个新个体被在其之前创建的任意新个体直接阻塞,而不仅仅局限于其祖先。通过对算法的可终止性、合理性和完备性进行证明,算法的正确性得以确认。In order to decide ABox consistency for description logic SHIN, a Tableau algorithm is presented. Given a TBox T, an ABox A and a role hierarchy H, the algorithm converts A into a standard ABox A＇ by pre-disposal, and then applies a set of Tableau rules to A＇ according to specific completion strategies until A＇ is extended to a complete ABox A＂. A is consistent with T and H, if and only if the algorithm can yield a complete and clash-free ABox A＂. A blocking mechanism adopted by the algorithm can avoid infinite execution of Tableau rules. The mechanism allows a new individual to be directly blocked by any in-dividual created before it, which is not restricted to its ancestor. Through proving the termination, soundness and completeness of the algorithm, its correctness can be confirmed.

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

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]