Font Size: a A A

Machine Proofs For Affine Geometric Theorems Of Constructive Type Based On Mass Point Method

Posted on:2016-07-11Degree:MasterType:Thesis
Country:ChinaCandidate:H J SuFull Text:PDF
GTID:2180330470468921Subject:Applied Mathematics
Abstract/Summary:PDF Full Text Request
Geometric theorem proving is a hot topic in the field of automated reasoning,Researchers have made great achievements in the study of geometry theorem proving aspect in recent years.Since Wu’s method published in 1977, the researches and practises for automated proving of geometry theorems have been achieved many breakthroughs.Typically, the proving methods of geometric theorem can be divided into three categories:algebraic method, artificial intelligence method and geometric invariant method.Algebraic method is to prove the advantages of high efficiency, the disadvantage is poor readability;although artificial intelligence is readable but inefficient and incomplete;the readability of geometric invariant method is between algebraic method and artificial intelligence.Particle geometry uses more abstract objects- particles, as the basic geometric elements.Mr. Mo have described particle geometry theories and methods systematically.In order to develop a particle geometry with better readability, more efficient geometric theorem proving approach provides operational basis.The mass point method, which based on basic principles and properties of the mass point geometry, is a complete algorithm for constructive geometry theorems. It has the advantages of high running efficeint, good readability, easy to implement and so on.This paper describes an improvement on the mass point method which proves constructive affine geometry theorems.Firstly,an elimination method was advanced from known equations to target equations;Secondly,an complete elimination process was established by modules.Finally, conclusion statement was judged by undetermined coefficient method.Elimination process of MPP prover is more concise than the original mass point method and has obvious geometric meaning.The algorithm is implemented with Matlab and tested with 10 geometric theorems of constructive type.The experimental results show that it is more efficient than ever before.
Keywords/Search Tags:Mass Point Geometry, Elimination Method, Machine Proof, Automated Geometry Reasoning
PDF Full Text Request
Related items