Automated Geometry Theorems Proving And Discovering Based On Point Geometry

Intelligent problem solver is an important research field in artificial intelligence.With the further development of education informationization,education resources are required to be intelligent rather than simply "electronical".Educational software lacks of intelligence or is not sufficiently intelligent,which makes it difficult to meet the needs of teaching.Developing highly intelligent educational software has the key to solving these issues,among which intelligent problem solver is the core technology.Machine proof of geometric theorem is a branch of intelligent solver.In order to make the outcome of intelligent solvers play a better role in teaching and learning,our research mainly focuses on two goals:improving the readability of machine solutions and discovering more novel geometric propositions.Our contributions are as follows:Firstly,a point geometry identity algorithm is proposed.On the basis of learning Wu's method,point geometric operations are used to express the geometric relationship concisely and transformed into a vector polynomial.The equation is solved by the undetermined coefficient method,and the identities that can correlate the propositional conditions and the conclusion are explored.The generated algebraic identities have obvious geometric meaning,and a new bridge is constructed between numbers and shapes.The principle of this method is simple,the calculation is easy,the proof given is understandable,and the reader needs little basic knowledge.Therefore,it basically achieves the "self-evident proof " goal.Most proofs are even shorter than the original questions and clearly show the relationship between the conditions and conclusions,so they can be extended from one question to multiple questions,and from low dimensions to high ones.Secondly,a hybrid reasoning algorithm based on point geometry identities.In order to make better use of the advantages of different solutions,combined with algebraic calculations and search ideas,two algorithms for mining hidden relationships are proposed,which greatly expands the scope of problem solving by the identity method.For some long-discussed ordered geometric problems,give a short identity proof,we point out the necessary and sufficient conditions for the proposition establishment,and expand the proposition from multiple angles;while previous solutions need to introduce more new concepts,complex operations,and fail to reach the same effect.A point geometry solution system was developed for constructable geometric problems,which generated readable proofs with detailed steps.The traversal search function,especially in combination with the extended drawing function,can discover and prove geometric propositions in batches,and also search for the necessary conclusions to supplement the identity algorithm.Thirdly,a vector equation elimination algorithm is proposed.Based on Euler's formula in the complex number form,the geometric relationship is transformed into vector equations,and then the basic properties of linear equations are used to eliminate the vector.And it extracts the coefficient matrix containing the relationship between the side length and the angle,calculating the determinant and simplifying,calling the element elimination method to eliminate variables that are not of interest,and obtains some geometrically meaningful relations.This is a new idea that combines algebraic methods with invariants.Using this method to study some classic geometric figures not only reproduces the classic conclusions,but also finds the conclusions that are hidden in the figures which were ignored by senior mathematicians.This method is good at discovering and proving edge relationships in the form of polynomials,which fills the gap in previous studies.Especially for the study of a single triangle,a large number of triangle identities can be generated automatically or mandatorily.Fourthly,a geometric problem bank has been established.In order to validate the algorithm,we sorted out more than 1,000 representative geometric problems.After these typical cases were processed by the algorithm in this paper,many new conclusions were found,which enriched the content of a problem and greatly enhanced the quality of a problem.It helps students to practice variant exercises,strengthen and consolidate key and difficult concepts or skills.For the convenience of teachers and students,we have published a series of articles and works based on the problem bank.Most of the problems are collected manually,and a small part is automatically generated by the computer.To make it easier to read,only a few conjunctions and analysis are inserted by human.The solutions are so understandable that reviewers and readers do not even notice that they are mainly generated automatically by the computer.This fully demonstrates that the automatic generated solutions can be understood and accepted in the education field.Our research shows that human solver may not be the best,and computers may give surprisingly good answers.The computer may gives an answer even shorter than the question,which seems to be contrary to common sense,but it also causes people to think about how knowledge can be represented as concise and convenient as possible for reasoning.The innovative representation of knowledge should conform to the requirements of the information age as much as possible,and may also cause the relocation of the original knowledge system.