-
题名Taylor展开式与三角函数不等式的自动证明
被引量：6
- 1
-
-
作者
陈世平
刘忠
-
机构
中国民航飞行学院德阳校区-四川省商贸学校
乐山职业技术学院
-
出处
《系统科学与数学》
CSCD
北大核心
2016年第8期1339-1348,共10页
-
基金
德阳市校(院
所)市科技合作计划资助课题
-
文摘
文章以具有模型f(x,tan(x/2))>0的三角函数不等式为研究对象来探讨超越不等式的机器证明问题,运用Taylor展开式将目标不等式的证明转化为一系列的一元多项式不等式的证明,然后借助代数不等式证明工具(如Bottema)完成最后的工作.运用Maple编制程序实现了上述算法,实验结果表明算法对常见的三角函数不等式十分有效,并且证明过程是"可读"的.
-
关键词
超越不等式
三角函数不等式
机器证明
上限多项式
下限多项式
可读证明
-
Keywords
Transcendental inequality, trigonometric function inequality, mechanical proving, upper limit polynomial, lower limit polynomial, readable proving.
-
分类号
O178
[理学—数学]
-
-
题名指数多项式不等式的自动证明
被引量：3
- 2
-
-
作者
陈世平
刘忠
-
机构
中国民航飞行学院德阳校区-四川省商贸学校
乐山职业技术学院
-
出处
《系统科学与数学》
CSCD
北大核心
2017年第7期1692-1703,共12页
-
基金
德阳市校(院
所)市科技合作计划资助课题
-
文摘
讨论了指数多项式不等式的自动证明问题,运用Taylor展开式将目标不等式的证明转化为一系列的一元多项式不等式的验证,然后借助代数不等式证明工具(如Bottema)完成最后的工作.运用Maple实现了上述算法,算法对所有指数多项式不等式终止,并且可以输出"可读"的证明过程.
-
关键词
指数多项式不等式
自动证明
上限多项式
下限多项式
可读证明.
-
Keywords
Exponent polynomial inequalities, automated proving, upper limit poly-nomial, lower limit polynomial, readable proving.
-
分类号
O174.14
[理学—数学]
-
