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

Autoři: Peter Franek
doc. Dipl. Ing. Stefan Ratschan, Dr. tech.
Rok vydání: 2016
Typ publikace: Článek v odborném periodiku
Periodikum: Journal of Automated Reasoning
Projekty: Integrovaná verifikace a falzifikace hybridních systémů průmyslové velikosti
Efektivní zacházení s nelineárními numerickými omezeními vyskytujícími se v automatické dedukci o bohatých modelech počítačových systémů.
Výpočet robustních invariantů hybridních dynamických systémů s využitím simulací
Bibliografická citace: FRANEK, Peter, RATSCHAN, Stefan, ZGLICZYNSKI, P. Quasi-Decidability of a Fragment of the First-Order Theory of Real Numbers. Journal of Automated Reasoning. 2016, 57(2), 157-185. ISSN 0168-7433. E-ISSN 1573-0670
Dostupné z: doi:10.1007/s10817-015-9351-3
DOI: 10.1007/s10817-015-9351-3
ID: 449388

Abstrakt

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.