Automatically Solving Semi-algebraic Systems

Abstract

By ``semi-algebraic system'' mean a system consists of polynomial equations, polynomial inequations and polynomial inequalities, where all the polynomials are of real coefficients. Usually we ``solve'' such a system in three senses as follows:

(1) When the number of the equations is equal to or greater than that of the variables, we call it a constant-coefficient system, and a finitely many of isolated solutions is expected. It is required in this case to find the real solutions numerically.
(2) When the number of the equations is less than that of the variables, we call it a parametric system, and some manifold solutions with positive-dimensions are expected. It is required in this case to decide whether the system has any real solution or not.
(3) Furthermore, for a parametric system, it is often required to find conditions on the parameters such that the system has a certain number of real solutions.

In this talk, some recent advances for the three issues are demostrated by relevant programs in automatic mode, which have extensive applications to various fields including Automated Theorem Proving and Automated Theorem Discovering in real algebra and real geometry.