Machine Proofs in Geometry Based on Complex Number Method

With the rapid development of machine proofs in geometry, more and more geometric automated machine proving methods were proposed. But when dealing with some difficult geometric problems which involve a great number of symbolic computation, the existing machine proving programs failed because of the information explosion or the complexity of the algorithm. Thus a new machine proving method, the complex number method, is proposed. By choosing the software Mathematica which has powerful capability of symbolic computation, a new prover CNMP(complex number method prover) is created. The CNMP can easily solve all the 180 geometric problems on TGTP, which is a Web-based library of problems in geometry. It aims to become a comprehensive common library of problems with a significant size and unambiguous reference mechanism, easily accessible to all researchers in the automated reasoning in geometry community. The laboratory report shows that the CNMP is very effective and the readability is also satisfying. In particular, the CNMP can prove some very difficult geometric theorems, such as five circles theorem, Morley theorem, Lemoine circle theorem, Thebault theorem, Brocard circle theorem and so on.