Readable Proving for Geometric Theorems of Polynomial Equality Type
Jian-Guo JIANG, Jing-Zhong ZHANG, Xiaojing Wang · Chinese Journal of Computers · 2009
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.