In Eliminate Quantifiers, I wrote about George E. Collin's Quantifier Elimination for real closed fields. The method he introduced is Cylindrical algebraic decomposition (cad).
It is a major concept of symbolic computation and theoretically it could be applied to collision detection (see One Size Fits All? briefly mentioning the application of the Simplex algorithm to collision detection). But the complexity of cad is enormous.
