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
Webmaster: kamweb.mff.cuni.cz Modified: 19. 10. 2010