单变元三角函数不等式的发现与自动证明

何灯，李云杰

（福清第三中学，福建福清350315）

单变元三角函数不等式的发现与自动证明

何灯，李云杰

（福清第三中学，福建福清350315）

借助于级数理论和maple数学软件，本文研究单变元三角函数不等式的发现及机器自动证明，根据算法所编写的程序hdtrig2015能够在极短的时间内实现三角函数不等式的自动验证.丰富的实例表明本文的算法具有极大的优越性，能够成批实现三角函数不等式的机器自动验证.

三角函数；不等式；泰勒展开；机器证明；实根隔离

0　引言

不等式的发现与机器证明，一直是数学机械化、自动推理及智能系统领域的研究难点和热点问题，近年来得到了长足的发展[1-17].特别是杨路教授提出了降维算法[2-3，9，14]，据之编写的通用程序BOTTEMA能够成批验证和发现不等式.BOTTEMA的开发极大地影响着不等式研究者的研究方式和研究方法，但B0TTEMA只能处理代数不等式或先把几何不等式转化为代数不等式，尚不能解决一般的超越不等式自动证明问题，杨路教授也曾指出：B0TTEMA目前尚不适合处理类似sinx＜x＜tanx（0＜x＜/2）这样的超越不等式，这是值得进一步研究的课题[14].

三角函数不等式的证明是初等不等式证明问题的难点，因为不仅要运用代数不等式的方法，而且要使用三角函数的许多性质，如正余弦函数的有界性、三角函数的单调性等，各种三角函数之间的变换在证明不等式过程中的目的性、规律性不强，还有一些特殊方法不易机械化[5]，受这种种因素的限制，三角函数不等……