Elementary recursive quantifier elimination based on Thom encoding and sign determination

TL;DR

This paper introduces an elementary recursive quantifier elimination algorithm for real closed fields that relies on Thom encoding and sign determination, avoiding the use of connected components of semialgebraic sets.

Contribution

The paper presents a novel algebraic quantifier elimination method with elementary recursive complexity, distinct from existing approaches that use connected components.

Findings

Algorithm has elementary recursive complexity

Proof of correctness is purely algebraic

Connected components are not used in the approach

Abstract

We describe a new quantifier elimination algorithm for real closed fields based on Thom encoding and sign determination. The complexity of this algorithm is elementary recursive and its proof of correctness is completely algebraic. In particular, the notion of connected components of semialgebraic sets is not used.