A Complete Algorithm for Automated Discovering of a Class of Inequality-type Theorems

WR algorithm, Wu's elimination and a partial cylindrical
algebraic decomposition, we present here a practical algorithm
for automated inequality discovering which can discover
new inequalities automatically, without requiring us to put
forward any conjectures beforehand. That is complete for
an extensive class of inequality-type theorems. Also this
algorithm is applied to the classification of the real physical
solutions of geometric constraint problems. Many inequalities
with various backgrounds have been discovered or re-discovered
by our program, DISCOVERER, which implements the algorithm in
Maple.