Quasi-decidability of a Fragment of the First-order Theory of the Real Numbers and Topological Extension of Maps to the Sphere

Stefan Ratschan a Peter Franek

MÚUK

Abstract

The first-order theory of the real numbers is decidable in the polynomial case, while including more general functions like sin makes the problem undecidable.

We study a fragment of this theory that allows such functions, and that includes systems of m polynomial equations in n real variables. We are interested in robust formulas, that is, formulas whose satisfiability is stable with respect to small perturbations of the formula. An example of a robust formula is x=0 whereas a non-robust formula is x^2=0. More generally, we say that a formula is robust, if its satisfiability does not change under small perturbations.

We prove that (under the additional assumption that all variables range over closed intervals) there is a (possibly non-terminating) algorithm for checking satisfiability of a system of m equations in