《计算机学报》文章摘要   全文下载
文章题目	多项式等式型几何定理的可读证明
作者	江建国1),2) 张景中2) 王晓京2)
作者单位	1)(辽宁师范大学数学学院 辽宁大连 116029) 2)(中国科学院成都计算机应用研究所 成都 610041)
发表年份	2008
发表月份	2期(207—213)
文章摘要	摘要 目前的智能几何软件都使用基于搜索法的定理证明器作为推理引擎，其主要缺点是不能可读地证明涉及到几何量代数运算的几何定理，这极大地限制了智能几何软件的实际应用.对一类结论为几何量多项式等式的几何定理，文中提出了一种能给出可读证明的启发式搜索算法.该算法通过引入多项式的变形操作算子——标准项代换，把证明结论为多项式等式g=0的几何定理转化为寻找从g到0的标准项代换序列的搜索问题.采用Lisp语言实现了该算法，并做了30个结论为几何量等式的几何定理的推理实验.实验结果表明算法具有较高的推理效率. 关键词 几何定理机器证明；搜索法；标准项代换；启发函数；可读证明 中图法分类号 TP181