基于Rete算法的几何自动推理系统

智能几何教学软件都使用基于前推法的几何推理系统作为推理引擎。推理引擎的主要工作是做推理规则和几何信息的匹配计算。推理过程中产生的大量冗余匹配严重地影响了推理效率。为了提高推理引擎的推理效率, 作者首次将Rete模式匹配算法整合到推理引擎中, 构造了一种高效的几何自动推理引擎, 称为几何自动推理网。几何自动推理网通过消除推理过程中的冗余匹配达到了提高系统推理效率的目的。使用Lisp语言编写了几何自动推理网程序iGeo, 并做了50多个非平凡几何定理的推理实验, 实验结果表明iGeo具有更高的推理效率。

The Automated Geometry Reasoning System Based on Rete Algorithm

The automated geometry reasoning system based-on forward chaining is used as the reasoning engine in the intelligent geometry teaching system. The reasoning engine spends much time match geometry information to rules in the reasoning process and then decreases the reasoning efficiency of the system seriously. In order to improve the efficiency of the reasoning engine, a new geometry theorem proving method, named automated geometry reasoning network was put forward,in which the Rete pattern matching algorithm is integrated into the reasoning engine. The reasoning efficiency can be improved by eliminating redundancy computation on matching geometry information to rules in the reasoning process. The reasoning program based on the automated geometry reasoning network method, named iGeo, was implemented in Lisp. The iGeo was tested with more than 50 nontrivial geometry theorems. The experimental results demonstrated that the iGeo is very efficient.