¡¡	Chinese Journal of Computers   Full Text
Title	Readable Proving for Geometric Theorems of Polynomial Equality Type
Authors	JIANG Jian-Guo1),2) ZHANG Jing-Zhong2) WANG Xiao-Jing2)
Address	1)(Mathematics School, Liaoning Normal University, Dalian, Liaoning 116029) 2)(Chengdu Institute of Computer Applications, Chinese Academy of Sciences, Chengdu 610041)
Year	2008
Issue	No.2(207¡ª213)
Abstract &   Background	Abstract Currently the automated reasoning engineer of the intelligent geometry software is limited in the theorem prover based on search method. A drawback is that it can not give the readable proving for geometric theorems involving algebraic computation. A heuristic search algorithm using the standard item substitute is presented in this paper, which can give readable proving for a class of geometric theorems as long as its conclusions are polynomial equalities about geometric quantities, such as the length of segment, the degree of angle. The algorithm is implemented with Lisp and tested with 30 nontrivial geometry theorems. The experimental results show that it is more efficient than ever before. keywords automated geometry theorem proving; search method; item substitute; heuristic function; readable proof background The project is supported by the National Basic Research 973 Program of China under grant No.2004CB318000. The long-term goal is to build intelligent geometry software for school£¬ which can be helpful to teachers and students. Any proofs produced by the software must be stated with the common ontology of Euclidean geometry¡ª¡ªThe axiom geometry taught in schools. There are mainly two approaches to proving geometry theorems using computers: the artificial intelligence (AI) approach, like search methods, point elimination methods, and the algebraic computation (AC) approach, like Wu¡¯s methods, Gr¢‰ber base methods. Generally speaking, the AC approaches are decision procedures and are more powerful. The AI approaches are not decision procedures. But proofs produced by the AI approaches are more readable than the AC approaches. Thus the AI approaches are more suitable for intelligent geometry software. In fact, two pieces of intelligent geometry software, named Geometry Experts and Super Sketchpad, are developed in recent years. Now both are used in a lot of middle schools in China, and were warmly welcomed by teachers and students. The automated reasoning engineer of the intelligent geometry software is usually limited in the theorem prover based on search method. A drawback is that it can not give the readable proving for geometric theorems involving algebraic computation. This paper presents a high efficient algorithm for the search method that can give readable proving for a class of geometric theorems as long as its conclusions are polynomial equalities about geometric quantities, such as the length of segment, the degree of angle.