In early 30s A. Tarski, motivated by a problem of automatic theorem proving
in elementary algebra and geometry, suggested an algorithm
for quantifier elimination in the first order theory of the reals.
The complexity of Tarski's algorithm is a non-elementary function of
the format of the input formula.
In mid-70s a group of algorithms appeared based on the idea of a cylindrical
cell decomposition and having an elementary albeit doubly-exponential
complexity, even for deciding closed existential formulae.
The tutorial will explain some ideas behind a new generation of algorithms
which were designed during 80s and 90s and have, in a certain sense, optimal
In a useful particular case of closed existential formulae (i.e., deciding
feasibility of systems of polynomial equations and inequalities) these
new algorithms are theoretically superior to procedures known before in
numerical analysis and computer algebra.
© 2002-2003 Kurt Gödel Society, Norbert Preining.