基于语义网的几何自动推理研究及其应用

摘要

几何自动推理是让计算机模拟人脑来进行几何命题的证明，它是人工智能领域的重要研究课题。20世纪70年代，吴文俊先生就提出了定理机器证明的方法；随后，张景中院士在面积法的基础上发展了消点法。这些方法都使自动推理的研究取得了突破性进展。但是，从目前的推理软件来看，关于几何命题的证明还存在一些问题：一是上述方法与传统几何命题的证明方法不符，二是机器还不能完全学会几何学家的解题技巧，如辅助线、辅助点的添加。
　　如何设计一种自动推理的方法，使其在保证效率的前提下，既能符合传统证明方法，又能与几何学家相媲美，成为当前重要的研究课题。为了实现自动推理，本文引入了语义网的相关理论与技术，首先，使用本体对平面几何证明过程和推理规则进行构建，生成本体模型，然后，通过模型匹配，并借助辅助信息库的查询来实现自动推理。主要研究内容如下：
　　1、平面几何知识表示。首先，通过对几何命题证明过程的深入研究，自动化地对每一个因果分段进行概括模型和详细模型的提取，并将模型存储于过程本体中。其中，概括模型体现了因果分段的抽象化描述，详细模型体现了因果分段的实例化描述。接着，为了解决辅助线、辅助点的相关问题，对几何推理规则进行了深入研究，使用Protégé构建了基于平面几何学科知识的领域本体，该领域本体为辅助信息库提供相关信息。
　　2、平面几何知识推理。针对不需要辅助信息就能完成的几何证明，为了提高效率，先使用逆向推理，通过与概括模型的匹配来判断是否可能有解，在条件成立的情况下，再使用正向推理，通过与详细模型的匹配来获得证明过程。针对需要辅助信息才能完成的证明，将通过辅助信息库的查询来获取新条件，以此来增大推理成功率。为了提高推理效率，关于辅助线的添加，在辅助线信息库中只存放不存在连线生成的新条件，而关于辅助点的添加，则根据解题经验设计相关算法，并采用边添加边删除的策略。
　　最后，本文通过实验展示了过程本体与领域本体的构建，并将其成功地应用于需要添加辅助线、辅助点才能解决的自动推理实例中。

目录

封面

声明

中文摘要

英文摘要

目录

第一章 绪论

1.1 研究背景及意义

1.2 研究现状

1.3 研究内容

1.4 论文组织结构

第二章 相关理论与技术

2.1 语义网

2.2 本体论

2.3 描述逻辑与语义查询

2.4 本体构建

2.5相关工具

2.6 本章小结

第三章 基于平面几何的本体构建研究

3.1 平面几何本体知识库的结构

3.2 基于平面几何的过程本体构建

3.3 基于平面几何的领域本体构建

3.4 本章小结

第四章 几何自动推理算法的研究与设计

4.1自动推理的分析

4.2 基于过程本体的自动推理

4.3 基于领域本体的自动推理

4.4 本章小结

第五章 实验与结果分析

5.1 实验概述

5.2本体的构建

5.3自动推理实验分析

5.4对比Math-xp证明分析

5.5本章小结

第六章 结论与展望

6.1 总结

6.2 展望

致谢

参考文献

攻硕期间取得的研究成果