Quantifier elimination and cylindrical algebraic decomposition - Caviness, Bob F.; Johnson,Jeremy R (Texts and monographs in symbolic computation, 1998)