基于矩形区域剖分的不等式机器证明方法—以Zirakzadeh的一个几何不等式为例  

A MECHANICAL PROOF TO A GEOMETRIC INEQUALITY OF ZIRAKZADEH THROUGH RECTANGULAR PARTITION OF POLYHEDRA

作　　者：曾振柄[1] 张景中[2] 

机构地区：[1]华东师范大学上海高可信计算重点实验室,上海200062 [2]中国科学院成都计算机应用研究所自动推理实验室,成都610041

出　　处：《系统科学与数学》2010年第11期1430-1458,共29页Journal of Systems Science and Mathematical Sciences

基　　金：973课题(2004CB318003);国家自然科学基金(10471044);国家自然科学基金重点项目(90718041);上海市重点学科建设项目(B412)

摘　　要：1988年,张景中,陶懋颀用细致的人工估计,用BASIC语言程序在PB700微型计算机上证明了Zirakzadeh于1964年证明的一个几何不等式,其方法是把不等式涉及的变量所在之区域剖分为一系列充分小的矩形,在每个小矩形上用数值方法验证若干三角函数不等式的正确性.这个工作后来没有发表,将Zirskzadeh不等式转化为一个有3个变元的根式不等式,形如m_1^(/2)+m_2^(/2)+m_3^(/2)≥3m_4^(/2),其变量所在区域为一由6个线性不等式限制形成的多面体P(有14个顶点,21个棱和9个面),先用幂级数展开方法证明讨论的根式不等式在小长方体邻域[-0.1,0.1]~3C P成立,次将这个邻域以外的集合分割成有限多个边长不小于1/1280的小长方体或多面体,在每个小凸体上通过计算函数在顶点的取值和函数偏导数范围证明根式不等式的正确性.文章给出的验证数引理,可根据连续可微函数在长方体或一般凸多面体V的顶点的值,及函数偏导数的绝对值在集合V的上界,证明函数在V上的正定性.文章给出计算多项式在三维空间凸多面体上的最大值和最小值,以及估计根式函数的验证数的机械化方法.In this paper is concerned with a machine proof to the following geometric inequality,which was presented by A.Zirakzadeh in 1964：given any triangle ABC and three points P,Q,R,which divide the perimeter of ABC into three equal parts,the perimeter of PQR is equal to or greater than the one half of that of ABC.By representing the Zirakzadeh inequality as radical problem of form f（u,v,w） =（m_1）^（1/2）＋（m_2）^（1/2） ＋（m_3）^（1/2） -3（m_4）^（1/2）≥0,where m_1,m_2,m_3,m_4 are cubic polynomials of u,u,w and（u,v,w） belongs to a polyhedron P in R^3 with 14 vertices,21 edges and 9 faces,we first construct a cube B~＊ =[-0.1,0.1]~3C P and a polynomial g（u,v,w） of total degree 8 so that f（u,v,w）≥g（u,v,w） and g（u,v,w）≥0 in B~＊,then we prove two lemmas on error analysis for testing the positive definiteness of a continuous differentiable function on a rectangular region or a polytope through its values at the vertices,and finally we show the inequality f（u,v,w）0 for（u,v,w）∈P ／ B~＊ by partitioning the polyhedron into a finitely many small rectangular sets which edges are 1/（1280） or larger and the values of f（u,v,w） at the vertices of the rectangular sets exceed the test numbers for positive definiteness.The total computation time for the third step is 159.124 hours on personal computers.We also establish a mechanical method for computing the lower and upper bounds of polynomials and the test numbers of radical expressions over polyhedra in R^3.

关 键 词：数学机械化 机器证明 Zirakzadeh不等式 矩形剖分 误差分析 

分 类 号：O178[理学—数学]