Real quantifier elimination in practice

Abstract. We give a survey of three implemented real quantifier elimi-nation methods: partial cylindrical algebraic decomposition, virtual sub-stitution of test terms, and a combination of Gröbner basis computations with multivariate real root counting. We examine the scope of these im-plementations for applications in various fields of science, engineering, and economics.