Elementary recursive quantifier elimination based on Thom encoding and sign determination (Q529166)

In the paper under review, the authors describe a new quantifier elimination algorithm for real closed fields based on Thom encoding and sign determination whose complexity is elementary recursive. What is important, the proof of its correctness is entirely based on algebra and does not involve the notion of connected components of semialgebraic sets: for all previously existing elementary recursive methods, the proofs of correctness of the algorithms had been based on geometric properties of semialgebraic sets. The development of algebraic proofs is very important in the field of constructive algebra. In particular, it is important to provide an elementary recursive algorithm for quantifier elimination over real closed fields, suitable for being formally checked by a proof assistant such as Coq.