差分代换与不等式机器证明  

Difference substitution and automated inequality proving

作　　者：杨路[1] 

机构地区：[1]广州大学计算机教育软件研究所,广东广州510006

出　　处：《广州大学学报（自然科学版）》2006年第2期1-7,共7页Journal of Guangzhou University:Natural Science Edition

基　　金：国家重点基础研究发展规划项目(2004CB318003);国家自然科学基金项目(NNSFC-10471044)资助

摘　　要：设计了一个试探性的计算机程序SDS,用于证明多项式不等式,或等价地,用于判定多项式的非负性.将各变量按一定方式分割成较小的非负量,将变量替换后的多项式合并同类项,然后看是否所有的系数都是非负的.该方法不是完备的,但实验结果表明该程序对许多情况有效.不少次数较高或变量较多的多项式,除了SDS,还没有任何其他软件能做.A program named SDS is designed for polynomial inequality proving, in other words, for decision of nonnegativity of polynomials. The basic idea is： split the variables into smaller nonnegative quantities, then, collect the terms and see whether the coefficients all are nonnegative. The method has been used to prove symmetric＇ polynomial inequalities for so many years that the origin is unavailable. This is a heuristic, not a complete algorithm. However, it was demonstrated to be very efficient in practice. Quite a number of polynomial inequalities was not proven until program SDS is employed.

关 键 词：不等式机器证明 半正定 差分代换 平凡非负性 差分代换平凡 

分 类 号：TP3[自动化与计算机技术—计算机科学与技术]