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

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

文中讨论了一类根式不等式的有理等价问题.证明了这类根式不等式可等价转化为一组有理不等式.建立了一个算法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.