Elementary recursive quantifier elimination based on Thom encoding and\n sign determination

2016/09/09 by Daniel Perrucci, Perrucci, Daniel, Marie-Françoise Roy +1
Computer Science · Engineering · #03C10 #14P10 #Advanced Numerical Analysis Techniques #Algebraic Geometry (math.AG) #Computational Complexity (cs.CC) #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Numerical Methods and Algorithms #Polynomial and algebraic computation

paper · pdf · doi:10.48550/arxiv.1609.02879

openalex publication_date 2016/09/09 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

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

Related

• A Quantifier Elimination Algorithm for Linear Real Arithmetic
• Applying Linear Quantifier Elimination
• Quantifier elimination for the reals with a predicate for the powers of two
• Quantifier elimination for quasi-real closed fields
• Quantifier elimination and minimality conditions in algebraically closed valued fields