多项式等式型几何定理的可读证明

Readable Proving for Geometric Theorems of Polynomial Equality Type

目前的智能几何软件都使用基于搜索法的定理证明器作为推理引擎,其主要缺点是不能可读地证明涉及到几何量代数运算的几何定理,这极大地限制了智能几何软件的实际应用.对一类结论为几何量多项式等式的几何定理,文中提出了一种能给出可读证明的启发式搜索算法.该算法通过引入多项式的变形操作算子——标准项代换,把证明结论为多项式等式g=0的几何定理转化为寻找从g到0的标准项代换序列的搜索问题.采用Lisp语言实现了该算法,并做了30个结论为几何量等式的几何定理的推理实验.实验结果表明算法具有较高的推理效率.

Currently the automated reasoning engineer of the intelligent geometry software is limited in the theorem prover based on search method. A drawback is that it can not give the readable proving for geometric theorems involving algebraic computation. A heuristic search algorithm using the standard item substitute is presented in this paper, which can give readable proving for a class of geometric theorems as long as its conclusions are polynomial equalities about geometric quantities, such as the length of segment, the degree of angle. The algorithm is implemented with Lisp and tested with 30 nontrivial geometry theorems. The experimental results show that it is more efficient than ever before.