Elementary recursive quantifier elimination based on Thom encoding and sign determination
DOI10.1016/j.apal.2017.03.001zbMath1373.14060arXiv1609.02879OpenAlexW2962899356MaRDI QIDQ529166
Daniel Perrucci, Marie-Françoise Roy
Publication date: 18 May 2017
Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1609.02879
Fields related with sums of squares (formally real fields, Pythagorean fields, etc.) (12D15) Semialgebraic sets and related spaces (14P10) Effectivity, complexity and computational aspects of algebraic geometry (14Q20) Quantifier elimination, model completeness, and related topics (03C10)
Related Items (1)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Thom's lemma, the coding of real algebraic numbers and the computation of the topology of semi-algebraic sets
- On computing the determinant in small parallel time using a small number of processors
- The complexity of elementary algebra and geometry
- Solving systems of polynomial inequalities in subexponential time
- Real quantifier elimination is doubly exponential
- On the computational complexity and geometry of the first-order theory of the reals. III: Quantifier elimination
- Complexity of deciding Tarski algebra
- A new decision method for elementary algebra
- Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
- Improved Algorithms for Sign Determination and Existential Quantifier Elimination
- On the combinatorial and algebraic complexity of quantifier elimination
- Decision procedures for real and p‐adic fields
- Algorithms in real algebraic geometry
This page was built for publication: Elementary recursive quantifier elimination based on Thom encoding and sign determination
