常用基本不等式的机器证明

来源 :智能系统学报 | 被引量 : 0次 | 上传用户：akiheeca

【摘要】

：

不等式机器证明问题是智能系统领域的难点和热点问题.借助不等式证明软件BOTTEMA,对若干常用的基本不等式成功地实现了机器证明,包括算术、几何与调和平均不等式、排序不等式

【作者】

：

杨路郁文生

【机构】

：

华东师范大学上海高可信计算重点实验室

【出处】

：

智能系统学报

【发表日期】

：

2011年05期

【关键词】

：

基本不等式机器证明不等式证明软件BOTTEMA Tarski模型

下载到本地 , 更方便阅读

下载此文赞助VIP

声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架

论文部分内容阅读

不等式机器证明问题是智能系统领域的难点和热点问题.借助不等式证明软件BOTTEMA,对若干常用的基本不等式成功地实现了机器证明,包括算术、几何与调和平均不等式、排序不等式、Chebyshev不等式、Bernoulli不等式、三角形不等式及Jensen不等式等.所论不等式含有的变元个数是一个不确定的变量,属于Tarski模型外的不等式类型.机器证明得出的结论有时可能是已知结果的推广,其方法本身对同类不等式有示范性,更多的例子表明了该算法和软件的有效性.

其他文献

同向锥体锥角的测量

文章介绍了利用正弦尺测量同向锥体和锥角的测量方法。

期刊

同向锥体锥角测量测量装置示意图

团队人口统计特征多元化与绩效关系的元分析

Harrison和Klein(2007)将团队人口统计特征多元化划分为分离、多样和不平等三种类型。借鉴这一分类,运用元分析的方法检验了不同类型的团队人口统计特征多元化对团队绩效的影

期刊

团队多元化分离多样不平等绩效

论惩罚性赔偿——经济法具体责任研究

经济法作为新兴的法律部门 ,应当具有其独立的法律责任形式 ,惩罚性赔偿就是经济法的一种具体责任形式。惩罚性赔偿制度在英美法系国家已广泛适用 ,而我国仅在《消费者权益保

期刊