Practically solving some problems expressed in the first order theory of real closed field

Abstract

Many important mathematical and engineering problems can be expressed in the first order theory of real closed field Th(RLC), however any decision method for this theory needs exponential time even using nondeterministic computation models. Therefore it is desirable to find practical and efficient methods (non-decision methods) of solving problems expressed in this theory. By combining Ritt-Wu′ method with Budan-Fourier′s theorem, we propose a method to practically solve some problems expressed in this theory. In our method Budan-Fourier′s theorem is used to provide information on real roots of polynomial equations and to prove polynomial inequalities to hold, which is simpler and more efficient than Sturm theorem that is used in decision methods for Th(RLC). Our method has been found to efficiently work on many examples in practice though it is incomplete in general. Using our method, we have solved some problems, including deriving some new conditions on the existence of eight limit cycles for a cubic differential system which can not be dealt with using conventional methods because of the complexity of manipulating large polynomials. In this paper we describe our method by presenting some algorithms and examples.

Keywords:

• Real closed field
• Symbolic computation
• Ritt-Wu's method
• Budan-Fourier's theorem

C.R. Categories:

• I.1

^∗Corresponding author.

^∗Corresponding author.

Notes

^∗Corresponding author.

Additional information

Notes on contributors

Shilong Ma

a