Towards fast one-block quantifier elimination through generalised critical values

International audienceOne-block quantifier elimination is comprised of computing a semi-algebraic description of the projection of a semi-algebraic set or of deciding the truthof a semi-algebraic formula with a single quantifier. Until now, it has been tackled in practice by using variants and improvements of theCylindrical Algebraic Decomposition (CAD) algorithm. For example, see the software packages QEPCAD, RegularChains or the system Mathematica. This algorithmic framework suffers from a complexity that is doubly exponential in the dimension of the ambient space. However, it has been shown that one-block quantifier elimination can be performed within a complexity that is singly exponential in that dimension