几何定理的机器证明是自动推理领域的热门课题之一,尤其是近些年来,研究者在研究几何定理机器证明方面取得了丰硕的成果。吴文俊先生在1997年提出了“吴法”,几何定理机器证明的研究因而取得了重大突破。通常,几何定理机器证明方法可分为代数法,人工智能法和几何不变量法三大类。代数法的优点是证明效率高,缺点是可读性差;人工智能法虽然可读性好但不完备、效率低;几何不变量法的可读性介于代数法和人工智能法之间,其证明效率与代数法也在伯仲之间。质点几何使用了比几何不变量更抽象的对象——质点,作为基本几何元素。莫绍揆先生在《质点几何学》一书中系统地阐述了质点几何的方法和理论。质点几何支持对点直接进行线性运算,在处理仿射几何问题时较为方便,为发展出一种效率更高、可读性更好的几何定理机器证明方法提供了可操作的依据。质点法是一种利用质点几何的基本原理和基本性质来证明构造型几何定理的完备性算法,具有运行效率高、可读性好、易于实现等优点。本文针对质点法生成的目标质点关系式的过程不简明,缺少明显的几何意义的问题,提出了一种具有较高可读性算法的几何定理证明器MPP。为了进一步提高质点法的可读性和证明能力,具体提出了两大改进:一个是直接使用消点公式来推导目标质点关系式,另一个是利用待定系数法来统一地判定结论质点等式的正确性。基于改进后的质点法设计了该款几何定理证明器,并采用Matlab语言实现了该证明器。由于可以对点直接进行运算,证明器MPP的消点过程比原有质点法简明,具有更加明显的几何意义。在计算机上采用Matlab语言作了10个构造型仿射几何定理的运行实验,实验结果表明该证明器具有较高的运算效率。