一类根式不等式的有理化算法与机器证明  

Rationalizing Algorithm and Automated Proving for a Class of Inequalities Involving Radicals

作　　者：徐嘉[1] 姚勇[1] 

机构地区：[1]中国科学院成都计算机应用研究所,成都610041

出　　处：《计算机学报》2008年第1期24-31,共8页Chinese Journal of Computers

基　　金：国家"九七三"重点基础研究发展规划项目基金(2004CB318003);中国科学院知识创新工程重要方向项目(KJCX-YW-S02)资助

摘　　要：文中讨论了一类根式不等式的有理等价问题.证明了这类根式不等式可等价转化为一组有理不等式.建立了一个算法RFD,并用Maple编程实现.对一个给定的这类根式不等式,RFD可自动快速地产生一组有理等价不等式.将RFD算法和差分代换方法相结合,给出了一大类具有相当难度的几何不等式的机器证明.此前该课题仅有的工作是杨路关于二次根式的结果.A theory is developed to transform a class of inequalities involving radicals to a set of rational inequalities. And this theory is implemented by a Maple program named ＂RFD＂ which can efficiently produce a set of rational inequalities that equal to the original inequalities involving radicals. Combining RFD with SDS, the program can automatically prove an extensive class of geometric inequalities involving radicals.

关 键 词：根式不等式 有理化 不等式机器证明 差分代换 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]