| 【论文摘要】 | 几何定理的机器证明是自动推理和符号计算领域最为活跃的分支之一。在几何定理机器证明方法中,常用的有几何代数方法、演绎数据库方法和例证法等方法。其中,数学机械化思想的倡导者吴文俊院士提出的几何定理的代数证明方法,被认为是具有开创性意义的方法,带来了几何定理机器证明的新发展。近年来,随着计算机容量的扩大和计算速度的不断更新,计算机在数学领域的应用也不断深入,另一种几何定理机器证明方法—定理机器证明的数值方法,也得到了蓬勃发展。在该领域,先后出现了数值并行法、例证法、单例试验法等多种用数值方法对几何定理进行机器证明的方法,使得定理机器证明领域更得到了广阔的发展。然而,上述几何定理机器证明方法主要针对等式型定理的证明,不等式型定理的机器证明则一直是自动推理领域中的一个难题。
上世纪50年代初,Tarski发表了著名的《初等代数与初等几何的判定问题》,宣称在理论上可以解决实几何问题,但由于其方法复杂度太高效率太低不能实现。随后,Collins提出了柱面代数分析方法(CAD),效率得到了提高,能证明一些稍难的几何不等式;吴方法出现后,有人将吴方法与Lagrange乘子法结合,用求极值的方法处理一些有关不等式的几... |
