«上一篇/Previous Article|本期目录/Table of Contents|下一篇/Next Article»

《计算机技术与发展》[ISSN:1006-6977/CN:61-1281/TN]

卷:

24

期数:

2014年08期

页码:

89-93

栏目:

智能、算法、系统工程

出版日期:

2014-08-10

文章信息/Info

Title:

 Realization of Geometry Theorem Proving with Ontology and AllegroGraph

文章编号:

1673-629X（2014）08-0089-05

作者:

 吴店年; 李云清

 江西师范大学 计算机信息工程学院

Author(s):

 WU Dian-nian; LI Yun-qing

关键词:

 ; 本体推理; AllegroGraph(AG) ; Prolog规则; 几何; 定理证明

Keywords:

 ; ontology reasoning; AllegroGraph (AG); Prolog rules; geometry; theorem proving

分类号:

TP301

文献标志码:

A

摘要:

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

Abstract:

 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 a-nalysis 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 theo-rem 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.

常用功能

更新日期/Last Update: 2015-03-26