A complete algorithm for counting real solutions of polynomial systems of equations and inequalities

We present a complete and practical algorithm which can determine the number of distinct real solutions of a given polynomial system of equations and inequalities with integer coefficients mechanically. Based on this algorithm, a program called nearsolve has been implemented in Maple. The algorithm and program have been successfully applied to many problems with various backgrounds and to automated discovering and proving for inequality-type theorems.