Christopher W. Brown
This paper provides a relatively brief introduction to quantifier elimination by cylindrical algebraic decomposition (CAD). It's primarily taken from my Ph.D. thesis, which is already a few years old (gulp!). So this does not necessarily reflect the current state of the art.