摘要: 本文首先定义了标准三角恒等式,给出了证明标准三角恒等式的一个完备算法。最后介绍了在Alpha机上已实现的SJZM程序。它是用来证明经简单整理可与标准三角恒等式等价的一类三角恒等式的启发式程序。其输出的证明三角恒等式的步骤与教科书中书写的格式类似。H.Gelernter、J.R.Hansen和D.W.Loveland于50年代研究了几何定理证明的启发式程序,James R.Slae设计出了求符号积分的启发式程序,取得了令人满意的成果。美国已广泛地应用了电子计算机进行辅助教学。从应用计算机进行辅助教学这一目的出发,我们研究了采取经验探索法,应用计算机证明三角恒等式的算法和程序。