| Dynamic geometry software (DGS) is di?erent from general drawing softwareessentially. DGS allows users to creat accurately and manipulate interactivelygeometry diagrams, such as moving the position of free points, and explore itsproperties. So, DGS can help students to learn geometry and explore geometrystatements interactively. Also, teachers can teach geometry with the help ofDGS on computer which is better than traditional instruction. It has been apowerful tool for teaching and learning geometry. It has great impact on geometryeducation nowadays.However, DGS's shortcomings disclosed by the application in daily educa-tion. It is the main drawback that DGS is lack of intelligence, which is thebottleneck of DGS's application. Here, "intelligence" means that DGS can helpusers to solve geometry problems like experts. This paper calls this kind of soft-ware as intelligent geometry software (IGS). IGS can not only construct dynamicgeometry diagrams but also solve geometry problems automatically. So, it iscapable of aiding students to learn geometry proofs better than before.With the aid of the research fruits from the automated geometry theoremproving, this paper can implement the software with intelligence mentioned aboveby embedding the geometry theorem prover (GTP) in the DGS. At present, IGShas been used by teachers and students in many middle schools, such as GeometryExpert, Super Skatchpad, Experience Mathematics—Math XP.The GTP is the essential program in the IGS. Currently, most of IGS uses theGTP based-on forward chaining method as reasoning engine, because this methodis able to produce traditional proofs that can be understood and checked bystudents. However, forward chaining method has many disadvantages, such thatthe overhead of reasoning really costs, and the power of solving problems is weak.In order to improve reasoning e?ciency and enforce power, three refinementtechniques have been proposed in this paper:1. An e?ective matching reasoning engine for forward chaining method bythe introduction of Rete algorithm, namely automated geometry reasoningnetwork (AGRN), is proposed in this paper. The AGRN transforms therule base into the data-?ow network that stores the matching status in thereasoning process. This method eliminates redundant computations in thematching process to improve the reasoning e?ciency.2. In order to improve the e?ciency of reasoning geometry equivalence infor-mation by forward chaining method, This paper present the equivalenceclass reasoning approach, which including two techniques: Firstly, it usesrules of merging equivalence class to replace transitivity rules of geomet-ric equivalent predicate. Secondly, it uses rules of replacing equivalenceclass to replace rules of geometric equality predicate. In addition, This pa-per try to theorize the foundation of equivalence class reasoning and makequantitative analysis in its in?uence on reasoning process.3. This paper proposes a kind of heuristic equation reasoning algorithm whichcan produce traditional proving for a class of geometric statements whoseconclusions are polynomial equalities of geometric quantities, such as lengthsof segments, degrees of angles, areas of triangles etc. This algorithm changesthe problem of deriving equation e1 = e2 into the procedure of searchingthe item substitute path from e1 ? e2 to 0. Essentially, it is a sort of A?algorithm.This paper designed and implemented a geometry theorem prover iGeobased on forward reasoning method, into which the three techniques as mentionedabove are integrated. The iGeo is tested with more than 60 nontrivial geometrystatements. The experimental results demonstrate that the iGeo can not onlyact e?ciently and powerfully but also produce traditional proofs of many knowngeometry theorems such as Gauss theorem, Stewart theorem, Ptolemy theorem,etc. These theorems can not be proved by existing geometry theorem proversbased on forward reasoning method.Thus, the IGS using the iGeo as its reasoning engine is more appropriateto satisfy the needs of teachers and students.
|
PDF Full Text Request