Machine Proof Of Particle Geometry Theorem

Geometric theorem proving is a hot research topic in the field of automated reasoning,which is of great theoretical significance and practical application value.After Wu's method published,many new methods have been put forward such as area method,vector method,exemplification method and particle method.The particle method is a method based on the particle whose principal conception is as belows.Firstly,the geometric theorem is described in a constructive way and its result is described as a formula of particles.Secondly,the constrained particles in the particles formula are eliminated one by one until only three particles left based on the opposite order of particle introduction.Finally,the final result is obtained by the method of undetermined coefficients.Particle method has many advantages such as high efficiency,good readability,easy to implement and so on.However,the current particle method ability is limited,which can only prove that the structure geometry representation theorem of linear relationship equation conclusion available particle,other than that relate to the length or area of geometrical theorem such as the median line theorem,field problem etc.In this paper,the limitation of the particle method has been improved.On one hand,adding a simplified algorithm for the expression of volume type particles.On the other hand,calling different reduction algorithm in the process of eliminating points according to different conclusion of the particle.On the basis of these two improvements,a new algorithm called VE algorithm is presented,which can prove not only the geometric theorem of linear particle,but also the geometric theorem of volume ratio.Based on the improved particle method,a new geometric theorem prover PGP(Particle Geometry Prove)is designed and implemented using Matlab.The machine have proved more than ten particle geometry theorems.The results show that the proof of the automatic generation of the PGP prover has higher readablility and wider application.