Automated Geometry Readable Proving Based on Vector
Qian Ge · Chinese Journal of Computers · 2014
Many novel methods have been successfully developed in the field of automated geometry theorem proving,however,those based on the vector representations did not seize some basic characteristics of geometric vectors,and therefore have not given full play to the advantages of the vector method.To solve this problem,upon the concept of loop of vectors,we propose a new vector-based readable automated geometry reasoning method in this paper.Moreover,we have implemented the corresponding software for automated theorem proving.For conventional Euclidean geometric problems,this software can construct geometry figure instantly.Furthermore,it can perform automated reasoning with various rules in the vector method according to the corresponding types of constructions.More importantly,the proofs generated by our software are concise and readable.The Experimental results show that the proposed method is efficient and effective.Compared with other provers such as Super Sketchpad,our prover greatly improves the proving ability and readability.Hence,our method not only enriches the current methods for geometry theorem proving,it also could be further developed into an education software and used in geometry education.