Noon lecture

list of noon lectures ( 2005 | 2006 | 2007 | 2008 | 2009 | 2010 | 2011 | 2012 | 2013 | 2014 | 2015 | 2016 | 2017 | future lectures)

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

MUK

Abstract

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

list of noon lectures ( 2005 | 2006 | 2007 | 2008 | 2009 | 2010 | 2011 | 2012 | 2013 | 2014 | 2015 | 2016 | 2017 | future lectures)

Webmaster: kamweb.mff.cuni.cz         Modified: 19. 10. 2010