作　　者： ; ; ;

机构地区： 华东师范大学软件学院上海市高可信计算重点实验室

出　　处： 《中国科学：信息科学》 2011年第1期48-65,共18页

摘　　要： 将一类积分不等式转化为Tarski模型外的齐次对称多项式不等式,该类齐次对称多项式的次数是给定的,变元个数可以是任意多个,并且多项式的系数是与变元个数相关的变系数.这些特点与杨路等人最近提出的几个公开问题密切相关,是比较有代表性的一类齐次对称多项式.然后利用Timofte关于对称多项式不等式判定的降维方法,结合不等式证明软件BOTTEMA及差分代换方法,给出对应的一类Tarski模型外的齐次对称多项式不等式的机器判定算法,从而实现原积分不等式的机器判定.当给定的积分不等式及齐次对称多项式不等式不成立时,可给出具体不成立的数值反例.应用例子表明问题的广泛性及算法的有效性. A class of integral inequalities is transformed into homogeneous symmetric polynomial inequalitiesbeyond Tarski model,where the number of elements of the polynomial,say n,is also a variable and the coeffcients are functions of n.This is closely associated with some open problems formulated recently by Yang et al.Using Timofte＇s dimension-decreasing method for symmetric polynomial inequalities,combined with the inequality-proving package BOTTEMA and a program of implementing the method known as successive difference substitution,we provide a procedure for deciding the nonnegativity of the corresponding polynomial inequality such that the original integral inequality is mechanically decidable;otherwise,a counterexample will be given. The effectiveness of the algorithm is illustrated by some more examples.

关 键 词： 积分不等式 对称多项式不等式 降维法 差分代换 机器判定 不等式证明软件

领　　域： [理学] [理学]