基于复数法的几何定理可读机器证明

Machine Proofs in Geometry Based on Complex Number Method

已有的机器证明方法在处理一些涉及大规模符号运算的几何问题时,常因算法复杂度过高或机器能力的限制,有时并不能在合理时间内实现可读机器证明.故提出了复数法这一新的几何定理机器证明算法,并选用符号计算功能较为强大的软件Mathematica创建了新证明器CNMP(complex number method prover).新提出的复数法能有效地解决构造型几何命题,对用于测试与评价几何定理证明器性能的综合性平台TGTP(thousands of geometric problems for geometric theorem provers)上的180个几何问题的实验结果表明,CNMP的解题能力与运行效率均令人满意.尤其是对于一些具有相当难度的几何定理,如五圆定理、Morley定理、Lemoine圆定理、Thebault定理、Brocard圆定理等,CNMP均能在短时间内给出可读机器证明.

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.