Abstract. Automated deduction in real geometry depends essentially upon semi-algebraic system solving. By "semi-algebraic system" we mean a system consisting of polynomial equations, polynomial inequations and polynomial inequalities, where all the polynomials are of real coefficients. Usually, we "solve" such systems at three levels.

1. To find the real physical solutions of a geometric constraint problem, we need solve a certain semi-algebraic system where the number of equations is greater than or equal to that of variables; we call it a constant-coefficient system. In this case, finitely many isolated solutions are expected, and it is required that the real solutions be found numerically.
2. To prove or disprove a geometric inequality, we need solve a certain semi-algebraic system where the number of equations is less than that of variables; we call it a parametric system. In this case, some manifold solutions of positive-dimension are expected, and it is necessary to decide whether the system has real solutions or not.
3. To discover geometric theorems of inequality type automatically, it is often required that conditions on the parameters of a parametric system be found such that the system has a specified number of real solutions.

This talk is mainly devoted to the second issue mentioned above. A practical algorithm for inequality proving is demonstrated by a Maple program, BOTTEMA, in automatic mode, which has extensive applications in various fields.