-
题名常用基本不等式的机器证明
被引量：12
- 1
-
-
作者
杨路
郁文生
-
机构
华东师范大学上海高可信计算重点实验室
-
出处
《智能系统学报》
2011年第5期377-390,共14页
-
基金
国家自然科学基金资助项目(61070048
60874010)
+5 种基金
国家自然科学基金委员会创新研究群体科学基金资助项目(61021004)
国家"863"计划资助项目(2011AA010101)
国家"973"计划资助项目(2011CB302802
2011CB302400)
上海市重点学科建设资助项目(B412)
上海市教育委员会科研创新资助项目(11ZZ37)
-
文摘
不等式机器证明问题是智能系统领域的难点和热点问题.借助不等式证明软件BOTTEMA,对若干常用的基本不等式成功地实现了机器证明,包括算术、几何与调和平均不等式、排序不等式、Chebyshev不等式、Bernoulli不等式、三角形不等式及Jensen不等式等.所论不等式含有的变元个数是一个不确定的变量,属于Tarski模型外的不等式类型.机器证明得出的结论有时可能是已知结果的推广,其方法本身对同类不等式有示范性,更多的例子表明了该算法和软件的有效性.
-
关键词
基本不等式
机器证明
不等式证明软件bottema
Tarski模型
-
Keywords
fundamental applied inequalities
automated proving
inequality-proving package BOTFEMA
Tarski model
-
分类号
TP181
[自动化与计算机技术—控制理论与控制工程]
-
-
题名一类积分不等式的机器判定
被引量：1
- 2
-
-
作者
杨路
郁文生
袁如意
-
机构
华东师范大学软件学院上海高可信计算重点实验室
中国科学院成都计算机应用研究所自动推理实验室
中国科学院自动化研究所综合信息系统研究中心
-
出处
《中国科学：信息科学》
CSCD
2011年第1期48-65,共18页
-
基金
国家自然科学基金(批准号:60874010,61070048,90718041)
中国科学院知识创新工程重要方向(批准号:KJCX-YW-S02)、中国科学院海外杰出学者基金
上海市教育委员会科研创新(批准号:11ZZ37)资助项目
-
文摘
将一类积分不等式转化为Tarski模型外的齐次对称多项式不等式,该类齐次对称多项式的次数是给定的,变元个数可以是任意多个,并且多项式的系数是与变元个数相关的变系数.这些特点与杨路等人最近提出的几个公开问题密切相关,是比较有代表性的一类齐次对称多项式.然后利用Timofte关于对称多项式不等式判定的降维方法,结合不等式证明软件BOTTEMA及差分代换方法,给出对应的一类Tarski模型外的齐次对称多项式不等式的机器判定算法,从而实现原积分不等式的机器判定.当给定的积分不等式及齐次对称多项式不等式不成立时,可给出具体不成立的数值反例.应用例子表明问题的广泛性及算法的有效性.
-
关键词
积分不等式
对称多项式不等式
Timofte降维法
差分代换
机器判定
不等式证明软件-bottema
-
Keywords
integral inequality
symmetric polynomial inequality
Timofte＇s dimension-decreasing method
successive difference substitution
mechanical decision
inequality-proving package bottema
-
分类号
O178
[理学—数学]
-
