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

0449388 - ÚI 2017 RIV NL eng J - Journal Article
Franek, Peter - Ratschan, Stefan - Zgliczynski, P.
Quasi-Decidability of a Fragment of the First-Order Theory of Real Numbers.
Journal of Automated Reasoning. Roč. 57, č. 2 (2016), s. 157-185. ISSN 0168-7433. E-ISSN 1573-0670
R&D Projects: GA ČR GCP202/12/J060; GA MŠMT OC10048; GA ČR GA15-14484S
Institutional support: RVO:67985807
Keywords : decidability * decision procedure * real numbers
Subject RIV: IN - Informatics, Computer Science
Impact factor: 1.636, year: 2016

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.
Permanent Link: http://hdl.handle.net/11104/0250958