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

摘要：

为判定描述逻辑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算法、阻塞机制、可终止性、合理性、完备性

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

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

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

页数：共8页

页码：308-315