Nonstandard decision methods for the solvability of real polynomial equations

For a multivariate polynomial equation with coefficients in a computable ordered field, two criteria of this equation having real solutions are given. Based on the criteria, decision methods for the existence of real zeros and the semidefiniteness of binaly polynomials are provided. With the aid of computers, these methods are used to solve several examples. The technique is to extend the original field involved in the question to a computable non-Archimedean ordered field containing infinitesimal elements. Project supported by the National Natural Science Foundation of China (Grant No. 19661002) and the Climbing Project.