三角函数不等式的自动证明  

Automated proving of trigonometric inequalities

作　　者：陈世平[1,2] 

机构地区：[1]中国民航飞行学院德阳校区 [2]四川省商贸学校,德阳618000

出　　处：《四川大学学报（自然科学版）》2013年第3期537-540,共4页Journal of Sichuan University(Natural Science Edition)

摘　　要：本文以三角函数不等式为研究对象来探讨超越不等式的机器证明问题,运用变量替换和函数的Taylor展开式将目标不等式代数化,然后借助BOTTEMA中强有力的代数不等式证明工具完成最后的证明.编制程序实现了上述算法,实验结果表明算法对常见的三角函数不等式十分有效,并且算法是"可读"的.The problem of mechanical proving about transcendental inequalities is discussed with the trigonometric inequalities as the research object. Using variable substitution and Taylor expansion,the target inequality is transformed to an algebraic one, and then proved by the powerful inequality-proving package BOTTEMA. The above algorithms are implemented on Maple,and experiments show that they are very effective for most trigonometric inequalities, furthermore the procedure is ＂readable＂.

关 键 词：超越不等式 三角函数不等式 自动证明 BOTTEMA 可读证明 

分 类 号：TP3[自动化与计算机技术—计算机科学与技术]