The degree-decreasing decomposition of symmetric forms with a program for algebraic inequality decision. 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 that 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 systems for polynomials. This approach is implemented into a Maple program named SymProve3, and can prove many algebraic inequalities with degrees in hundreds or terms in thousands. At last, SymProve3 is successfully applied to prove 209 elementary multivariate polynomial inequalities from the on-line book [{it Nguyen Duy Tung}, 567 nice and hard inequalities] within only 33 seconds.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element