论文部分内容阅读
几何定理机器证明已经成为自动推理领域内的一个研究热点,它具有十分重要的理论意义与实践应用价值。自“吴法”发表以来,研究者又提出了多种新的机器证明方法,如:面积法、向量法、例证法、质点法等。其中,质点法是一种直接以“质点”作为运算对象的方法,其基本思想是:首先,用构造性的方式表述几何定理,并将结论表示为质点关系式;其次,按照“质点”引入次序的相反顺序逐个地将质点结论等式中的约束“质点”消去,直到质点结论等式中只剩下基点为止;最后,通过待定系数法计算得到最终的结果。质点法具有效率高、可读性好、易于实现等优点,并且生成的证明可读性非常好。但是当前质点法的证明能力有限,仅能证明结论等式可用质点线性关系表示的构造型几何定理,不能证明涉及长度、面积等几何量的定理,如:中位线定理、井田问题等。本文针对质点法证明范围的局限性做了改进:一个是增加了一个针对容积型质点表达式的化简算法Vsimplify;另一个是在消点的过程中根据质点结论等式的不同类型调用不同的化简算法。在这两大改进的基础上提出了一种既可以证明线性质点几何定理,又可以证明容积比型质点几何定理的新算法。基于改进后的质点法,利用Matlab设计实现了一款新的几何定理证明器PGP(Particle Geometry Prove),并对十多个质点几何定理进行了机器证明实验。实验结果表明,PGP证明器自动生成的证明更简短、可读性也更好而且证明范围也更广。