A complete algorithm for automated discovering of a class of inequality-type theorems

摘要

Making use of the discriminant sequence for polynomials, WR algorithm, Wu's elimina- tion and a partial cylindrical algebraic decomposition, we present here a practical algorithm for automat- ed inequality discovering which can discover new inequalities automatically without requiring to put for- ward 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 rediscovered by our Program, DISCOVERER, which implements the algorithm in Maple.