基于本体的几何定理机器证明

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