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

ABox Consistency Decision Algorithm for Description Logic SHIQ

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

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

出　　处：《计算机工程》2013年第12期308-315,共8页Computer Engineering

基　　金：国家自然科学基金资助项目(61073191);湖南省教育厅科学研究基金资助项目(12C0593);湖南第一师范学院校级课题基金资助项目(XYS10N09)

摘　　要：为判定描述逻辑SHIQ的ABox一致性,提出一种Tableau算法。给定TBox T、ABox A和角色层次H,通过预处理将A转换成标准的ABox A’,按照特定的完整策略将一套Tableau规则应用于A’,从而不断地对A’进行扩展,直到将其扩展成完整的ABox A’’为止。A、T和H一致,当且仅当算法能产生一个完整且无冲突的ABox A’’。该算法采用的阻塞机制能防止Tableau规则被无限次执行,避免多余的规则应用。通过证明Tableau规则的执行次数为有限次,确认算法的可终止性。通过证明由A’’能构造一个同时满足A、T和H的解释,确认算法的合理性。通过证明Tableau规则的执行不会破坏A’与H的一致关系,确认算法的完备性。In order to decide ABox consistency for Description Logic（DL） SH1Q, a Tableau algorithm is presented. Given a TBox T, an ABox A and a role hierarchy H, the algorithm first 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, thus A＇ is extended continually, until it 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＂. The blocking mechanism adopted by the algorithm can prevent Tableau rules＇ unlimited execution, and avoid redundant rule application. By proving Tableau rules＇ execution times is limited, the algorithm＇s termination is ensured. By proving Tableau rules＇ excecution is unlikely to destroy the consistency between A＇ and H, the algorithm＇s soundness is ensured. By proving an explanation which satisfies A, T and H can be constructed in terms of A＂, the algorithm＇s completeness is ensured.

关 键 词：描述逻辑SHIQ ABox一致性判定 TABLEAU算法 阻塞机制 可终止性 合理性 完备性 

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