质点几何定理机器证明一直以来都是自动推理领域的研究课题,其证明方法和研究成果都具有明显的应用价值。近年来,研究者们依据质点几何的定理和性质提出了质点法、线性质点消去法等证明方法,并基于上述方法实现了能证明质点几何定理的证明器。目前质点法仍有不足之处,例如:不能证明涉及几何量(长度、面积等)的定理,无法直接通过消点推出结论,输出的证明可读性还较差等等。为解决这些问题,本文在质点法的基础上提出了一种新的质点几何定理机器证明方法——容积型质点消去法。该方法不仅能证明容积比型质点几何问题,而且能计算容积比。由于质点容积运算的引入,该方法不仅能在证明过程中边消点边化简,而且消点后能直接推出定理结论。因此,该方法输出的证明过程与传统解题过程更加相似,更加具有明显的几何意义。容积型质点消去法还借助了“消点”思想,因此输出的证明过程更加简短易懂,可读性更加令人满意。基于提出的新方法,本文借助MATLAB语言设计并实现了一个能证明容积比型质点几何定理的证明器PMP。并利用该证明器在计算机上进行了30多个容积比型的质点几何定理的推理实验。实验结果表明,该证明器不仅能自动生成简洁明了的可读证明,而且具有令人满意的证明效率。希望证明器PMP能成为质点几何定理机器证明的一个有力工具,并能够对以后研究几何定理机器证明或开发智能性理科教育软件有所帮助。