机器证明在近30年来取得了一系列令人瞩目的研究成果,尤其是不等式的机器证明在举步维艰的情况下取得了辉煌的发展,开创性的开发了不等式证明软件——BOTTEMA,它已经成为不等式证明领域中的一个新宠,将会引领不等式的发展,并取得更好的成果。本文第一章从BOTTEMA软件的背景、基本原理及算法开始介绍,论及了该软件的发展历程、展望和使用方法等。第二章中从当前学校不等式的教育现状剖析,论证了当前不等式教学的弊端和不足,又鉴于时代发展和教学实际的需要,得出亟需在高校中引入一本适合的不等式新教材的结论。接着,我们详细地将最新数学机械化理论和BOTTEMA的底层算法、基本知识、使用方法、技巧、不等式可读证明和附加知识都编进了教材,设计了相应的章节和内容,并对该教材编写了配套的课程标准和教学建议。第三章中,从课堂教学的实际出发,以该教材为案例,论述了该部分引入教学的方法与期望效果,分别给出了实际的例子并细致地加以分析,同时也用实例的方式说明了BOTTEMA软件在不等式命题中的作用,又进一步得出这些新的思想方法对学生思维进步的促进作用。在此过程中,难免会遇到一些难点,所以,本章接着又预测了可能出现的问题并提供了具体的建议和解决办法。第二章和第三章是全文的核心部分。第四章对本文工作的成果和意义加以总结,并指出笔者今后的研究方向。