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

• 作者: 陈世平
• 来源期刊: 四川大学学报（自然科学版）
• 学科: 工学
• 关键词: 超越不等式 三角函数不等式 自动证明 BOTTEMA 可读证明
• 年，卷（期）: 2013,（3）
• 所属期刊栏目: 电子信息科学
• 页码范围: 537-540
• 页数: 4页
• 分类号: TP3
• 字数: 3252字
• 语种: 中文
• DOI: 10.3969/j.issn.0490-6756.2013.03.021

摘要

本文以三角函数不等式为研究对象来探讨超越不等式的机器证明问题,运用变量替换和函数的Taylor展开式将目标不等式代数化,然后借助BOTTEMA中强有力的代数不等式证明工具完成最后的证明.编制程序实现了上述算法,实验结果表明算法对常见的三角函数不等式十分有效,并且算法是“可读”的.