Elementary recursive quantifier elimination based on Thom encoding and sign determination

DOI10.1016/J.APAL.2017.03.001zbMATH Open1373.14060arXiv1609.02879OpenAlexW2962899356MaRDI QIDQ529166FDOQ529166

Marie-Françoise Roy, Daniel Perrucci

Publication date: 18 May 2017

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1609.02879

Recommendations

• Improved Algorithms for Sign Determination and Existential Quantifier Elimination
• Quantifier elimination for real algebra -- the quadratic case and beyond
• Computer Science Logic
• On the combinatorial and algebraic complexity of quantifier elimination
• scientific article

zbMATH Keywords

quantifier eliminationreal closed fieldssign determinationThom encoding

Mathematics Subject Classification ID

Semialgebraic sets and related spaces (14P10) Effectivity, complexity and computational aspects of algebraic geometry (14Q20) Fields related with sums of squares (formally real fields, Pythagorean fields, etc.) (12D15) Quantifier elimination, model completeness, and related topics (03C10)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Algorithms in real algebraic geometry
• A new decision method for elementary algebra
• On computing the determinant in small parallel time using a small number of processors
• Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
• Title not available (Why is that?)
• Solving systems of polynomial inequalities in subexponential time
• On the combinatorial and algebraic complexity of quantifier elimination
• On the computational complexity and geometry of the first-order theory of the reals. III: Quantifier elimination
• Real quantifier elimination is doubly exponential
• Decision procedures for real and p‐adic fields
• Complexity of deciding Tarski algebra
• Thom's lemma, the coding of real algebraic numbers and the computation of the topology of semi-algebraic sets
• Improved Algorithms for Sign Determination and Existential Quantifier Elimination
• The complexity of elementary algebra and geometry

Cited In (1)

• An Elementary Recursive Bound for Effective Positivstellensatz and Hilbert’s 17th problem

Uses Software

• Coq

This page was built for publication: Elementary recursive quantifier elimination based on Thom encoding and sign determination

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q529166)