Point Geometry A Mechanistic Approach To Dealing With Two Classes Of Geometric Propositions

As an advanced intelligence activity,geometric reasoning naturally becomes one of the first problems in the field of artificial intelligence.After decades of development,machine proving of geometric theorem has achieved rich results,but it is not enough to meet the needs of mathematics education.Therefore,it is necessary to continue to explore new automatic reasoning algorithms for geometric theorems.In 2018,Zhang Jingzhong put forward the basic idea of "Point Geometry".Based on the basic idea of Point Geometry,this paper studies the mechanization method of Point Geometry to deal with two kinds of geometric statements.According to the basic operations of Point Geometry,five properties are selected as the basic rules to form a mechanized method for the Hilbert intersection point statements.To deal with the proposition of metric geometry,five special rules are developed to form a mechanized method for dealing with the linear constructive geometry statements.The mechanization method is programmed to form a mechanization algorithm PGM(Point-Geometry-Method)for two kinds of statements,which is implemented as a Point Geometry prover in Maple.In Point Geometry,the origin is introduced.Compared with Mass Point Geometry,the judgment of the origin should be added when the program is implemented.However,the introduction of the origin can make the output of the proof simpler and more flexible than the particle method.The running example of Point Geometry prover shows that for most topics,the program can give the derivation process in a very short time,and the proof process is almost consistent with manual calculation.There are five chapters in this paper.The first chapter summarizes the research status of geometric theorem machine proving and Point Geometry.In the second chapter,five basic rules of Point Geometry are determined,which can deal with the Hilbert intersection point statements mechanically.In Chapter 3,based on the definition of multiplicative point of complex number,five special rules are developed to deal with linear constructive geometric statements mechanically.In Chapter 4,the mechanization method is programmed to form a mechanization algorithm PGM,which is implemented as a Point Geometry prover in Maple.In the fifth chapter,we test the processing ability of the Point Geometry prover for the above two kinds of statements and the running time of 130 examples is counted.