几何定理的机器证明是自动推理和符号计算领域最为活跃的分支之一。在几何定理机器证明方法中,常用的有几何代数方法、演绎数据库方法和例证法等方法。其中,数学机械化思想的倡导者吴文俊院士提出的几何定理的代数证明方法,被认为是具有开创性意义的方法,带来了几何定理机器证明的新发展。近年来,随着计算机容量的扩大和计算速度的不断更新,计算机在数学领域的应用也不断深入,另一种几何定理机器证明方法—定理机器证明的数值方法,也得到了蓬勃发展。在该领域,先后出现了数值并行法、例证法、单例试验法等多种用数值方法对几何定理进行机器证明的方法,使得定理机器证明领域更得到了广阔的发展。然而,上述几何定理机器证明方法主要针对等式型定理的证明,不等式型定理的机器证明则一直是自动推理领域中的一个难题。 上世纪50年代初,Tarski发表了著名的《初等代数与初等几何的判定问题》,宣称在理论上可以解决实几何问题,但由于其方法复杂度太高效率太低不能实现。随后,Collins提出了柱面代数分析方法(CAD),效率得到了提高,能证明一些稍难的几何不等式;吴方法出现后,有人将吴方法与Lagrange乘子法结合,用求极值的方法处理一些有关不等式的几何问题,但这些方法通用性和效率不理想。1998年,杨路提出了基于胞腔分解的降维算法,这一算法能有效处理含参根式,并最大限度地缩减维数,使不等式证明能达到较高的效率。但是,这种降维方法较多地利用了实代数系统方法,因而在实现时对符号计算软件有很大的依赖性,也比较复杂。 在已有定理机器证明数值方法的启发下,侯晓荣提出了一种新的几何不等式自动生成和证明的方法,本文对该方法予以了具体的实现和测试,在该领域做了一次有意义的尝试。我们首先采用数值计算在例证法的基础上根据用户需求,猜测生成一些符合条件的几何不等式;然后引入区间计算这一数值计算方法,以此作为计算工具,用作图的方法完成对指定不等式的证明.由于采用了数值计算,使得系统效率有很大的提高,同时用区间计算的方法,也避免了计算机进行单纯数值计算时丢失数值信息的弊端;而后用作图的方法,能够使证明过程脱离符号计算软件和代数系统的束缚,达到简单明了的效果。我们在Windows平台上用Visual C++编程实现了该算法,达到了对方法有效性检验的目的,程序执行速度也表明其系统效率也是令人满意的。