作者投稿和查稿 主编审稿 专家审稿 编委审稿 远程编辑

计算机工程

• 开发研究与工程应用 • 上一篇    下一篇

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

彭 立,杨恒伏   

  1. (湖南第一师范学院信息科学与工程系,长沙 410205)
  • 收稿日期:2012-10-25 出版日期:2013-12-15 发布日期:2013-12-13
  • 作者简介:彭 立(1974-),男,讲师、硕士,主研方向:描述逻辑,语义Web;杨恒伏,副教授、博士
  • 基金资助:
    国家自然科学基金资助项目(61073191);湖南省教育厅科学研究基金资助项目(12C0593);湖南第一师范学院校级课题基金资助项目(XYS10N09)

ABox Consistency Decision Algorithm for Description Logic SHIQ

PENG Li, YANG Heng-fu   

  1. (Department of Information Science and Engineering, Hunan First Normal University, Changsha 410205, China)
  • Received:2012-10-25 Online:2013-12-15 Published:2013-12-13

摘要: 为判定描述逻辑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的一致关系,确认算法的完备性。

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

Abstract: In order to decide ABox consistency for Description Logic(DL) SHIQ, 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.

Key words: Description Logic(DL) SHIQ, ABox consistency decision, Tableau algorithm, blocking mechanism, termination, soundness, completeness

中图分类号: