基于本体与Prolog的平面几何定理证明

Geometry Theorem Proving on Ontology and Prolog

基于本体理论、本体模型等方面的研究,以一个平面几何定理证明问题为例,详细地描述了平面几何本体的构建过程、基于本体和Prolog规则的推理,及其在平面几何问题求解中的应用。实验结果表明,将本体应用于几何定理机器证明是一种行之有效的方法,该方法避开了以往的代数方法中多次反复判断的问题,更接近自然语言的描述,能明确地表达领域知识和实现概念分层,从而能快速地构建几何模型,还可以进行复杂关系间的推理,最终实现基于本体和Prolog规则的平面几何定理证明。

In this paper,we propose a method to solve the problem of geometry theorem proving based on ontology theory.We describe the process of ontology construction,the reasoning based on ontology and prolog rules,and an example of a geometry theorem proving.The result shows that theorem proving based on ontology is efficient.This approach has advantages such as avoiding determining the problem repeatedly,natural language more closely,expressing the domain knowledge and the concepts hierarchy clearly.In addition this method can execute reasoning of complex relationships,and ultimately accomplishes elementary geometry theorem proving on ontology and prolog rules.