基于吴方法的几何定理证明的恒等式方法
作者:邹宇,彭翕成,饶永生 单位:广州大学计算科技研究院,华中师范大学国家数字化学习工程技术研究中心 本文刊于: 《中国科学:数学》 2021年第0期
关键词:
吴方法 几何定理证明 恒等式方法 点几何Keywords:
Wu’s method,geometry theorem proving,identity method,point geometry
摘要
多年来通常认为以吴方法为代表的几何定理机器证明的坐标法给出的证明不可读,或不是图灵意义下的类人解答.其实,只要对吴氏的算法做不多的改进,即将命题的结论多项式表示为其条件多项式的线性组合,就能获得不依赖于理论、算法和大量计算过程的恒等式明证.这样的恒等式可以转化为其他更简明且更有直观几何意义的点几何形式或向量及其他形式,从而获得多种证明方法.这也证明了点几何恒等式明证方法对等式型几何命题的普遍有效性.
基金项目:
国家自然科学基金(批准号:11701118)资助项目
上一篇:点集拓扑学之杨忠道定理的一个机械化证明
下一篇:Optimal car-following control for intelligent vehicles using online road-slope a