THE DEGREE-DECREASING DECOMPOSITION OF SYMMETRIC FORMS WITH A PROGRAM FOR ALGEBRAIC INEQUALITY DECISION
Chen Sheng-li, Liangyu Chen · Xitong kexue yu shuxue · 2013
Mechanical inequality proving has been a hot and difficult point in the field of automated theorem proving.In this paper,we provide a mechanical algorithm for determining a polynomial inequality to be true or not.Firstly,the original inequality with n variables is processed by homogenizing and symmetrizing,and then equivalently reduced to a class of polynomial inequalities in a special form with symmetric decomposition and degree-decreasing method.If all coefficients are positive, then it means the inequality has been proved.Otherwise,it can be proven by the tools of cylindrical algebraic decomposition,such as QEPCAD and BOTTEMA,or be transferred into a set of polynomial inequalities only with n - 2 variables by making use of complete discrimination system for polynomials.This approach has been implemented into a Maple program named SymProve3,and can prove many algebraic inequalities with degrees in hundreds or terms in thousands.At last,SymProve3 has been successfully applied to prove 209 elementary multivariate polynomial inequalities from the book《567 Nice and Hard Inequalities》within only 33 seconds.