描述逻辑SHIF和SHIQ的Abox一致性判定算法研究

摘要

描述逻辑是一类表示知识的形式系统，因具有正式的语法和语义并支持基于语义的推理，它们在知识表示领域得到了广泛的应用。SHIF和SHIQ是基本的描述逻辑ALC的扩展，它们具有比ALC更强的表达力，能解决较为复杂的知识建模问题。ABox一致性问题是描述逻辑最重要的推理问题之一，但在研究中得到的关注较少。为解决SHIF和SHIQ的ABox一致性问题，本文针对这两种描述逻辑的ABox一致性判定算法进行了研究，取得了以下成果。
　　 提出了一种SHIF的ABox一致性判定Tableau算法，并证明了算法的正确性。为了判定ABox Ain是否与TBox T一致，该算法先通过预处理将Ain转换成标准的ABox As，然后按任意顺序将特定的Tableau规则应用于As，直到它成为完整的ABox。若算法能产生一个完整且无冲突的ABox，则它给出肯定的答案，否则给出否定的答案。算法所采用”改良阻塞”机制能对Tableau规则的应用进行限制，从而确保算法在输入对象只有无限模型的情况下仍能正确终止。通过对算法的合理性、可终止性和完备性进行证明，算法的正确性得以确认。
　　 提出了一种SHIQ的ABox一致性判定Tableau算法，并证明了算法的正确性。为了判定ABox Ain是否与TBox T和角色层次H一致，该算法先通过预处理将Ain转换成标准的ABox As，然后按任意顺序将特定的Tableau规则应用于As，直到它成为完整的ABox。若算法能产生一个完整且无冲突的ABox，则它给出肯定的答案，否则给出否定的答案。为确保终止，该算法也采用了改良阻塞这种机制。该算法的合理性和完备性的证明与前一种算法的证明类似，而它的可终止性证明采用了一种新的方法，该方法利用了良基关系的一个性质。
　　 实现了SHIQ的ABox一致性判定算法。首先将该算法改造成了确定性算法，并利用ABox树证明了改造后的算法是正确的，然后用程序实现了该算法。因为SHIF是SHIQ的子语言，所以该程序也可以判定SHIF的ABox一致性。

目录

声明

摘要

插图索引

第1章 前言

1．1 研究背景

1．2 研究现状

1．3 主要研究内容

1．4 论文的结构

第2章 描述逻辑ALC的相关研究

2．1 ALC的语法和语义

2．2 DLs的知识库

2．2．1 术语部件TBox

2．2．2 断言部件ABox

2．3 DLs的推理问题

2．3．1 与概念有关的推理

2．3．2 与ABox有关的推理

2．3．3 在推理中消除TBox

2．4 ALC的Tableau算法

2．4．1 判定概念可满足性的Tableau算法

2．4．2 判定ABox一致性的Tableau算法

2．5 小结

第3章 描述逻辑SHIF的ABox一致性判定算法研究

3．1 SHIF的四种新特征

3．2 SHIF的语法和语义

3．3 SHIF的ABox一致性判定算法

3．3．1 预处理

3．3．2 阻塞机制

3．3．3 Tableau规则

3．3．4 完整的ABox

3．4 算法正确性的证明

3．4．1 合理性的证明

3．4．2 可终止性的证明

3．4．3 完备性的证明

3．5 小结

第4章 描述逻辑SHIQ的ABox一致性判定算法研究

4．1 SHIQ的语法和语义

4．2 SHIQ的ABox一致性判定算法

4．3 算法正确性的证明

4．3．1 合理性的证明

4．3．2 可终止性的证明

4．3．3 完备性的证明

4．4 小结

第5章 SHIQ的ABox一致性判定算法的实现

5．1 将非确定性算法改造成确定性算法

5．2 算法的程序实现

5．2．1 程序的输入和输出

5．2．2 主要的数据结构

5．2．3 程序的结构

5．2．4 主要函数的说明

5．2．5 程序正确性的验证

5．3 小结

结论

参考文献

附录A 攻读学位期间所发表的学术论文目录

致谢