第3卷第2期广州大学学报自然科学版()Vol.3No.22004年4月JournalofGuangzhouUniversity(NaturalScienceEdition)Apr.2004文章编号:167124229(2004)0220097210计算机怎样证明几何不等式杨路(广州大学计算机教育软件研究所,广东广州510405)摘要:阐述了一个基于胞腔分解的不等式机器证明软件的原理、算法和使用方法,这一用Maple语言编写的程序能有效地处理含有根式的不等式型定理,对于Bottema等所著《几何不等式》一书中的大部分不等式定理的验证尤其高效.对一类代数结构较为简单的几何不等式,能令计算机自动生成和输出用自然语言写出的证明.关键词:自动证明;几何不等式;构造性几何定理;半代数系统;胞腔分解中图分类号:TP3文献标识码:A众所周知,有一个精彩的几何不等式是以20显函数q=f(p)来表示.世纪著名的几何学家Finsler和Hadwiger命名的:在FP中令p=1,得到q的一个多项式设一个三角形的边长为a、b、c,面积为S.-1+5q-4q2,求证下面的不等式它有两个正根1/4和1.又在CP中令p=1,得到222222它在和之间没有根于是边界曲线a+b+c≥43S+(b-c)+(c-a)+(a-b).7-3q,1/41.全部落在开区域D之外.这意味着,只要该不等这个定理有许多不同的证法,其中以Finsler和式对一个非等腰的三角形成立,它就普遍成立.Hadwiger最初的纯几何证明最为巧妙和匪夷所思.易验证该不等式对于边长为3、4、5的三角形成这里有如下一个几乎纯代数的证明.立,故其普遍真.证毕.证明该不等式左多项式(用p、q作参数)为对于没有任何准备的读者,以上证明是无法T2-4(p+q)T+4p2+8pq-192p+4q2-48q-1296,看懂的.主要是因为不明白其中一些术语的涵义,其右多项式为如“左多项式”“、右多项式”、“边界多项式”、“基本-T+6p+2q+36,多项式”“、结式”、“判别式”等等.不过,任何非浅故其边界多项式为显的定理的证明都建立在一连串的严格定义之16p2+96p-48q,上,其实“机器证明”这一研究方向所要做的正是我们记之为CP.尽量减少术语和定义.熟知的基本多项式FP是独特之处在于,上面这个证明是由计算机自-p2+4pq+p2q-4q2,动生成和打印出来的,没有丝毫人为的干预.由于将p>0、q>0和FP>0定义的开区域记为D.近期取得的进展,对于一类代数结构较为简单的CP和FP关于q的结式为几何不等式,我们已经能够令计算机自动生成和234-p-p-p,[1]8118输出用自然语言写出的证明.这样的证明足以它没有正根因此当时和没有公.,p>0,CPFP以假乱真,分不出是机器所作还是人工所为.这个共零点.能够自动证明或否定不等式的软件便是“BOT2另一方面,CP关于q的判别式是1,它没有TEMA”,它的原理、算法和使用方法,是本文所要正根.所以,边界曲线CP=0落在区域D中的部介绍的内容.分要么是空的,要么可以用一个定义在p>0上的收稿日期:2003-10-08基金项目:国家973计划(NKBRSF-G1998030602)和中国科学院知识创新工程资助项目作者简介:杨路(1936-),男,教授,计算机软件与理论和数学学科博士生导师,主要从事自动推理、智能软件技术和计算机数学研究.©1994-2010ChinaAcademicJournalElectronicPublishingHouse.Allrightsreserved.http://www.cnki.net98广州大学学报(自然科学版)第3卷法[8,9]、数值并行法[10～12]等等.特别是张景1机器证明的代数方法中[13～15]及其合作者关于几何定理可读证明自动生成的工作,使得机器自动产生的证明可以和几本文讨论的几何不等式都具有纯代数的结何学家手工所作的证明相媲美.这一突破使得机构,实质上是研究代数不等式.Hilbert在1900年器证明的这部分成果能被普遍地接受并付诸实际提出的第17问题猜想:任何正定的实系数多元多应用.项式都可以表成实系数有理分式的平方和,这一上述20年来所获进展[16]主要限于等式型定著名猜测于1926年被Artin所证实.但实际可操理的证明,而对不等式机器证明的研究则举步维作的“配平方”算法仍为研究热点.譬如下面这个艰.Chou、Gao等[17,18]将CAD等原有算法和吴方多项式,我们已经知道(从别的渠道)它是正定的,法相结合,在这方面做了有益的探讨.不等式机但要将它