| 基于矩形区域剖分的不等式机器证明方法-以Zirakzadeh的一个几何不等式为例 |
| |
| 引用本文： | 曾振柄,张景中.基于矩形区域剖分的不等式机器证明方法-以Zirakzadeh的一个几何不等式为例[J].系统科学与数学,2010,30(11). |
| |
| 作者姓名： | 曾振柄 张景中 |
| |
| 作者单位： | 华东师范大学上海高可信计算重点实验室;中国科学院成都计算机应用研究所自动推理实验室; |
| |
| 基金项目： | 973课题，国家自然科学基金，国家自然科学基金重点项目，上海市重点学科建设项目 |
| |
| 摘 要： | 1988年,张景中,陶懋颀用细致的人工估计,用BASIC语言程序在PB700微型计算机上证明了Zirakzadeh于1964年证明的一个几何不等式,其方法是把不等式涉及的变量所在之区域剖分为一系列充分小的矩形,在每个小矩形上用数值方法验证若干三角函数不等式的正确性.这个工作后来没有发表.将Zirskzadeh不等式转化为一个有3个变元的根式不等式,形如(((√)m1)+((√)m2)+((√)m3)≥3((√)m4),其变量所在区域为一由6个线性不等式限制形成的多面体P(有14个顶点,21个棱和9个面),先用幂级数展开方法证明讨论的根式不等式在小长方体邻域-0.1,0.1]3(∪)P成立,次将这个邻域以外的集合分割成有限多个边长不小于1/1280的小长方体或多面体,在每个小凸体上通过计算函数在顶点的取值和函数偏导数范围证明根式不等式的正确性.文章给出的验证数引理,可根据连续可微函数在长方体或一般凸多面体V的顶点的值,及函数偏导数的绝对值在集合V的上界,证明函数在V上的正定性.文章给出计算多项式在三维空间凸多面体上的最大值和最小值,以及估计根式函数的验证数的机械化方法.
|
| 关 键 词： | 数学机械化 机器证明 Zirakzadeh不等式 矩形剖分 误差分析 |
A MECHANICAL PROOF TO A GEOMETRIC INEQUALITY OF ZIRAKZADEH THROUGH RECTANGULAR PARTITION OF POLYHEDRA |
| |
| ZENG Zhenbing,ZHANG Jingzhong.A MECHANICAL PROOF TO A GEOMETRIC INEQUALITY OF ZIRAKZADEH THROUGH RECTANGULAR PARTITION OF POLYHEDRA[J].Journal of Systems Science and Mathematical Sciences,2010,30(11). |
| |
| Authors: | ZENG Zhenbing ZHANG Jingzhong |
| |
| Institution: | ZENG Zhenbing (East China Normal University,Shanghai 200062) ZHANG Jingzhong (Chengdu Institute of Computer Application,Chinese Academy of Sciences,Chengdu 610041) |
| |
| Abstract: | |
| |
| Keywords: | Mathematics mechanization machine proof Zirakzadeh inequality rectangular decomposition error analysis |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
