geometry with both quantified and quantifier-free variables, the process of finding an equivalent first-order formula in these quantifier-free variables is called quantifier elimination. When the first-order formula is a boolean combination of polynomial equations and inequalities, we can consider quantifier elimination as a problem in real algebraic geometry.

The algorithm specified by Tarski [@tarski] for quantifier elimination is highly resource intensive. So newer and more efficient algorithms have come up and replaced it. The fact that projections upon parameters of a semialgebraic set (semialgebraic set is defined as the solution space of polynomial equations and inequalities) are also semialgebraic (Tarski-Seidenberg principle) has led to Cylindrical Algebraic Decomposition (CAD) [@collins], which eventually became the standard algorithm for quantifier elimination. The time complexity of CAD algorithm is doubly exponential in the number of variables (both quantified and quantifier-free).

CAD is a recursive algorithm, which constitutes of a sequence of projections, followed by a sequence of constructions. It has undergone an extensive array of developments, such as Hong’s Partial CAD [@partialcad], Hong’s projection operator [@hongproj], Scott McCallum’s projection operator [@mccallumproj], etc. An application of Gröbner Bases to CAD to improve the time complexity is studied in [@qegrob]. There were also some efforts to 