Elementary recursive quantifier elimination based on Thom encoding and sign determination

We describe a new quantifier elimination algorithm for real closed fields based onThom encoding and sign determination. The complexity of this algorithm is elemen-tary recursive and its proof of correctness is completely algebraic. In particular, thenotion of connected components of semialgebraic sets is not used.Fil: Perrucci, Daniel Roberto. Consejo Nacional de Investigaciones Científicas y Técnicas. Oficina de Coordinación Administrativa Ciudad Universitaria. Instituto de Investigaciones Matemáticas "Luis A. Santaló". Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales. Instituto de Investigaciones Matemáticas "Luis A. Santaló"; Argentina. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales. Departamento de Matemática; ArgentinaFil: Roy, Marie Françoise. Universite de Rennes I. Institut de Recherche Mathematique de Rennes; Franci