Quasi-decidability of a Fragment of the First-Order Theory of Real Numbers

In this paper we consider a fragment of the first-order theory of the real numbers that includes systems of n equations in n variables, and for which all functions are computable in the sense that it is possible to compute arbitrarily close interval approximations. Even though this fragment is undecidable, we prove that-under the additional assumption of bounded domains-there is a (possibly non-terminating) algorithm for checking satisfiability such that (1) whenever it terminates, it computes a correct answer, and (2) it always terminates when the input is robust. A formula is robust, if its satisfiability does not change under small continuous perturbations. We also prove that it is not possible to generalize this result to the full first-order language-removing the restriction on the number of equations versus number of variables. As a basic tool for our algorithm we use the notion of degree from the field of topology.