Automated discovering and proving for geometric inequalities

Automated discovering and proving for geometric inequalities have been considered a difficult topic in the area of automated reasoning for many years. Some well-known algorithms are complete theoretically but inefficient in practice, and cannot verify non-trivial propositions in batches. In this paper, we present an efficient algorithm to discover and prove a class of inequality-type theorems automatically by combining discriminant sequence for polynomials with Wu's elimination and a partial cylindrical algebraic decomposition. Also this algorithm is applied to the classification of the real physical solutions of geometric constraint problems. Many geometric inequalities have been discovered by our program, DISCOVERER, which implements the algorithm in Maple.