中文摘要：

定理机器证明是人工智能研究的重要课题，又属知识工程的范畴。几何定理机器证明最早由Hibert提出，50年代初Tarski用代数方法证明了初等几何机械化的可能性；70年代末，吴文俊院士给出可在计算机上实现的代数特征列方法；随后，张景中院士提出具有可读性的几何不变量方法。这些方法属于代数消元法，而逻辑证明一直是人类的梦想，自60年代格兰特提出后一直进展甚微。最近张景中院士和申请人研究出基于规则的几何定理证明器，在教育领域取得了很好的应用。但此方法很难明确表达领域知识和实现系统分层。因此，本项目将从更一般的本体知识库出发，研究在领域层将通用本体和自然语言处理技术用于扩展核心本体，构建几何知识本体，提供模型化的领域知识；在推理层构建一个集本体、复杂逻辑和符号计算于一体的推理模型，更好地实现知识推理，促进知识的共享和重用，从而为几何定理机器证明提供一条新途径，也为类似领域知识的问题求解提供新思路。

结论摘要：

本项目从更一般的本体知识库出发，以“构建领域核心本体→通用本体扩展领域核心本体→自然语言处理技术扩展领域核心本体”的层层递进的方式，研究在领域层构建一个较完善的几何知识本体，提供模型化的领域知识；研究推理层的基于本体的推理与规则相结合的混合推理模型，进一步研究计算相关问题的解决方式，建立数值测试推理策略，研究辅助线和辅助点的问题，建立辅助点和辅助线的推理策略，更好地实现知识推理；在此基础上构建一个集本体、规则推理、符号计算、数值测试、辅助线/点的添加等策略于一体的几何定理证明器；本项目为几何定理机器证明提供一条新途径，也为类似领域知识的问题求解提供新思路。