应用本体和AllegroGraph实现几何定理证明

Realization of Geometry Theorem Proving with Ontology and AllegroGraph

由于传统的定理机器证明方法是基于规则的,使得定理证明出现几何信息增长迅猛,推理和计算效率低以及过程可读性差等问题。针对以上情况,提出了基于本体和AllegroGraph的几何定理证明方法。该方法通过本体构建几何定理命题模型,然后采用Prolog规则描述语言对几何定理性质进行描述,同时通过分析本体模型和规则描述的对应关系,提出定理规则半自动生成方法。最后以AllegroGraph(AG)图形数据库的推理机制为基础,完成几何定理证明。实验结果表明,将本体和AllegroGraph推理机应用于几何定理证明领域可以摆脱以往几何定理证明代数化问题,几何证明过程容易理解,同时合理地控制了信息的增长,支持定理可持续证明。

As traditional theorem mechanical proving methods are based on the rules,making the geometry theorem proving occurs rapid growth,reasoning and calculations inefficient,and process poor readability. For the above cases,a design method of the geometry theorem proving based on ontology and AllegroGraph is presented. This method constructs the model of geometric theorem proposition through ontology,and then uses the Prolog rule description language to describe the nature of geometry theorems. At the same time,through the analysis of the correspondence between ontology model and rules described,propose semi-automatic method for the generation of theorem rules. Finally complete geometric theorem proving based on AllegroGraph （ AG） ,taking the reasoning mechanism of graphic database as the foundation. The experimental results show that the ontology and the AllegroGraph inference engine used in the field of geometry theorem proving can get rid of geometry theorem proving algebraic, geometric proof process is easy to understand, reasonably control the growth of information and support sustainable prove theorem.