Quantifier elimination, decision algorithm, effectiveness vs non-effectiveness in semialgebraic geometry
Presenter
March 26, 2014
Abstract
Quantifier elimination, decision algorithm, effectiveness vs non-effectiveness in semialgebraic geometry
Michel Coste
Université de Rennes I
This will be mainly an expository talk on quantifier elimination and decision algorithm for the first order theory of reals (due to A. Tarski). Quantifier elimination is very important for the geometry of semialgebraic sets. Its algorithmic nature gives effectiveness results almost for free. Of course one has to work more if one wants more precise information than recursive bounds, for instance.This question of effectiveness will be illustrated with some examples, notably the Hauptvermutung which states that the semialgebraic triangulation of a semialgebraic set is essentially unique.