On 17.05.2012 at 12:20 in S6, there is the following noon lecture:
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
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 n variables such that
(1) whenever it terminates, it computes a correct answer, and
(2) it always terminates when the input is robust.
We call a problem for which such an algorithm exists, quasi-decidable.
We show how the quasi-decidability of a system of equations is closely connected to the problem of topological extension of a map to the sphere and give an overview of some known results for this problem. In particular, we concentrate on the simplest case when m=n, i.e. the number of equations equals the number of unknowns.
Modified: 19. 10. 2010