三角不等式的自动证明  

Automated Proving of Triangular Inequality

作　　者：陈世平[1] 张景中[2] 

机构地区：[1]四川大学信息管理系,成都610065 [2]中国科学院成都计算机应用研究所,成都610041

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

摘　　要：作者设计并实现了一个将三角函数转化为有理分式的高效算法,从而可将三角不等式化为有理不等式来证明,并保证了其可读证明的自动生成.讨论了算法的实现技术,分析了其复杂度与输出结果.The problem of the inequality's readable proof is still unsolved, within which the proving of triangular inequality is one of the most difficult. Authors presents an efficient algorithm that can transform triangular inequality into rational inequality and produce the readable proof automatically after integrating with other algorithms. Authors discuss its critical technology, time complexity and its output.

关 键 词：可读证明 计算机符号代数 变量归一算法 智能教育软件 

分 类 号：O174.51[理学—数学]