Chinese Journal of Computers   Full Text
Title	Rationalizing Algorithm and Automated Proving for a Class of Inequalities Involving Radicals
Authors	XU Jia YAO Yong
Address	(Chengdu Institute of Computer Applications, Chinese Academy of Sciences, Chengdu 610041)
Year	2008
Issue	No.1(24—31)
Abstract &   Background	Abstract 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. keywords inequalities involving radicals; rationalization; automated proving; SDS background This work is supported by the National Basic Research Program of China (973 Program) under grant No.2004CB318003, which title is "The High Performance Algorithms in Real Geometry and Real Algebra". This paper develops a theory which aims at transforming a class of inequalities involving radicals to a set of rational inequalities, and also presents an algorithm which can efficiently prove an extensive class of geometric inequalities involving radicals. The authors′ research is based on rationalization of radical expressions of index 2, which is solved by Yang Lu on the webpage: http://www.irgoc.org/bbs/dispbbs.asp?boardID=4&ID=12&page=1. If you are interested in automated reasoning, please see about the references.