Satisfiability of Systems of Equations of Real Analytic Functions is Quasi-decidable

Autoři: Peter Franek
doc. Dipl. Ing. Stefan Ratschan, Dr. tech.
Rok vydání: 2011
Typ publikace: Konferenční příspěvek (mezinárodní konf.)
Periodikum: Mathematical Foundations of Computer Science 2011
Projekty: 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ů.
Bibliografická citace: FRANEK, Peter, RATSCHAN, Stefan, ZGLICZYNSKI, P. Satisfiability of Systems of Equations of Real Analytic Functions is Quasi-decidable. In: MURLAK, F., SANKOWSKI, P., eds. Mathematical Foundations of Computer Science 2011. Berlin: Springer, 2011, S. 315-326. Lecture Notes in Computer Science, 6907. ISBN 978-3-642-22992-3. ISSN 0302-9743
Dostupné z: doi:10.1007/978-3-642-22993-0_30
DOI: 10.1007/978-3-642-22993-0_30
ID: 368130

Abstrakt

In this paper we consider the problem of checking whether a system of equations of real analytic functions is satisfiable, that is, whether it has a solution. We prove that there is an algorithm (possibly non-terminating) for this problem such that (1) whenever it terminates, it computes a correct answer, and (2) it always terminates when the input is robust. A system of equations of robust, if its satisfiability does not change under small perturbations. As a basic tool for our algorithm we use the notion of degree from the field of (differential) topology.