There is this book : "Quantifier Elimination and Cylindrical Algebraic Decomposition" edited by Caviness and Johnson. It appeared in 1998 by Springer in their series texts and monographs in symbolic computation. It contains the original decision method of Tarski, Collins's CAD and complexity issues by Renegar.