Matiyasevich, Yuri - In: Mathematics and Computers in Simulation (MATCOM) 67 (2004) 1, pp. 125-133
This is a short survey of known results about elimination of quantifiers over natural numbers, and some implications of these results on the power of computer algebra systems.