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

• 作者: 张景中 江建国 王晓京
• 来源期刊: 计算机学报
• 学科: 工学
• 关键词: 几何定理机器证明 搜索法 标准项代换 启发函数 可读证明
• 年，卷（期）: 2008,（2）
• 所属期刊栏目: 研究论文
• 页码范围: 207-213
• 页数: 7页
• 分类号: TP181
• 字数: 6494字
• 语种: 中文
• DOI: 10.3321/j.issn:0254-4164.2008.02.003

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张景中	中国科学院成都计算机应用研究所	198	416	10.0	18.0
2	王晓京	中国科学院成都计算机应用研究所	32	339	9.0	17.0
3	江建国	辽宁师范大学数学学院	17	88	4.0	9.0