一类积分不等式的机器判定  

Mechanical decision for a class of integral inequalities

作　　者：杨路[1,2] 郁文生[1,3] 袁如意[3] 

机构地区：[1]华东师范大学软件学院上海高可信计算重点实验室,上海200062 [2]中国科学院成都计算机应用研究所自动推理实验室,成都610041 [3]中国科学院自动化研究所综合信息系统研究中心,北京100190

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

基　　金：国家自然科学基金(批准号:60874010,61070048,90718041);中国科学院知识创新工程重要方向(批准号:KJCX-YW-S02)、中国科学院海外杰出学者基金;上海市教育委员会科研创新(批准号:11ZZ37)资助项目

摘　　要：将一类积分不等式转化为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.

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

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