E. Ábrahám, J. Abbott, B. Becker, A. M. Bigatti, M. Brain et al.,

T. Seiler and . Sturm, SC 2 : Satisfiability Checking Meets Symbolic Computation, Proc. CICM 2016, vol.9791, pp.28-43, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01648696

E. Abraham, J. Nalbach, and G. Kremer, Embedding the Virtual Substitution Method in the Model Constructing Satisfiability Calculus Framework, Proc. of the 2nd International Workshop on Satisfiability Checking and Symbolic Computation. CEUR Workshop Proceedings, 1974.

S. Dennis and . Arnon, Algorithms for the Geometry of Semi-Algebraic Sets, Comput. Sci. Dept, 1981.

S. Basu, R. Pollack, and M. Roy, On the Combinatorial and Algebraic Complexity of Quantifier Elimination, J. ACM, vol.43, pp.1002-1045, 1996.

C. W. Brown, QEPCAD B: A Program for Computing with Semialgebraic Sets Using CADs, ACM SIGSAM Bulletin, vol.37, pp.97-108, 2003.

W. Christopher, J. H. Brown, and . Davenport, The Complexity of Quantifier Elimination and Cylindrical Algebraic Decomposition, Proc. ISSAC, pp.54-60, 2007.

W. Christopher, M. Brown, and . Ko?ta, Constructing a Single Cell in Cylindrical Algebraic Decomposition, J. Symb. Comput, vol.70, pp.14-48, 2014.

W. Christopher, A. Brown, and . Strzebo?ski, Black-Box/White-Box Simplification and Applications to Quantifier Elimination, Proc. ISSAC 2010, pp.69-76, 2010.

K. Burhenne, Implementierung eines Algorithmus zur Quantorenelimination für lineare reelle Probleme, 1990.

G. E. Collins, Quantifier Elimination for the Elementary Theory of Real Closed Fields by Cylindrical Algebraic Decomposition, Automata Theory and Formal Languages. 2nd GI Conference, vol.33, pp.134-183, 1975.

G. E. Collins and H. Hong, Partial Cylindrical Algebraic Decomposition for Quantifier Elimination, J. Symb. Comput, vol.12, pp.299-328, 1991.
DOI : 10.1007/978-3-7091-9459-1_9

C. David and . Cooper, Theorem Proving in Arithmetic without Multiplication, Proc. 7th Annual Machine Intelligence Workshop. Machine Intelligence, vol.7, pp.91-99, 1972.

F. Corzilius, Integrating Virtual Substitution into Strategic SMT Solving. Doctoral Dissertation, 2016.
DOI : 10.1007/978-3-642-22953-4_31

F. Corzilius and E. Abraham, Virtual Substitution for SMT Solving, Proc. FCT 2011, vol.6914, pp.360-371, 2011.
DOI : 10.1007/978-3-642-22953-4_31

H. James, J. Davenport, and . Heintz, Real Quantifier Elimination is Doubly Exponential, J. Symb. Comput, vol.5, pp.29-35, 1988.

M. Davis, Final Report on Mathematical Procedures for Decision Problems, 1954.

A. Dolzmann, Algorithmic Strategies for Applicable Real Quantifier Elimination. Doctoral Dissertation, 2000.

A. Dolzmann, O. Gloor, and T. Sturm, Approaches to Parallel Quantifier Elimination, Proc. ISSAC, pp.88-95, 1998.
DOI : 10.1145/281508.281564

A. Dolzmann and T. Sturm, Guarded Expressions in Practice, Proc. ISSAC, pp.376-383, 1997.
DOI : 10.1145/258726.258851

A. Dolzmann and T. Sturm, Redlog: Computer Algebra Meets Computer Logic, ACM SIGSAM Bulletin, vol.31, pp.2-9, 1997.

A. Dolzmann and T. Sturm, Simplification of Quantifier-free Formulae over Ordered Fields, J. Symb. Comput, vol.24, pp.209-231, 1997.

A. Dolzmann and T. Sturm, P-adic Constraint Solving, Proc. ISSAC, pp.151-158, 1999.

A. Dolzmann and T. Sturm, Redlog User Manual, 1999.

A. Dolzmann and T. Sturm, Parametric Systems of Linear Congruences, Proc. CASC, pp.149-166, 2001.

A. Dolzmann, T. Sturm, and V. Weispfenning, A New Approach for Automatic Theorem Proving in Real Geometry, J. Autom. Reasoning, vol.21, pp.357-380, 1998.

A. Dolzmann, T. Sturm, and V. Weispfenning, Real Quantifier Elimination in Practice, Algorithmic Algebra and Number Theory, pp.221-247, 1998.

H. Errami, M. Eiswirth, D. Grigoriev, W. M. Seiler, T. Sturm et al., Efficient Methods to Compute Hopf Bifurcations in Chemical Reaction Networks Using Reaction Coordinates, Proc. CASC 2013, vol.8136, pp.88-99, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00931946

H. Errami, M. Eiswirth, D. Grigoriev, W. M. Seiler, T. Sturm et al., Detection of Hopf Bifurcations in Chemical Reaction Networks Using Convex Coordinates, J. Comput. Phys, vol.291, pp.279-302, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01239486

J. Fourier, Analyse des travaux de l'Académie Royale des Sciences pendant l'année 1824, Partie mathématique, Mémoires de l'Académie des sciences de l'Institut de France, vol.7, pp.xlvij-lv, 1827.

D. Grigoriev, Complexity of Deciding Tarski Algebra, J. Symb. Comput, vol.5, pp.65-108, 1988.

A. Grzegorczyk, Some Classes of Recursive Functions, Rozprawy Matematyczne, vol.4, pp.1-45, 1953.

C. Hoffelner, Quantifier Elimination-based Parametric Solving in Term Algebras, 2005.

K. Korovin, M. Ko?ta, and T. Sturm, Towards ConflictDriven Learning for Virtual Substitution, Proc. CASC 2014, vol.8660, pp.256-270, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01088450

M. Ko?ta, New Concepts for Real Quantifier Elimination by Virtual Substitution, 2016.

M. Ko?ta, T. Sturm, and A. Dolzmann, Better Answers to Real Questions, J. Symb. Comput, vol.74, pp.255-275, 2016.

A. Lasaruk, , 2005.

A. Lasaruk and T. Sturm, Weak Integer Quantifier Elimination Beyond the Linear Case, Proc. CASC 2007, vol.4770, 2007.

A. Lasaruk and T. Sturm, Weak Quantifier Elimination for the Full Linear Theory of the Integers, Appl. Algebr. Eng. Comm, vol.18, pp.545-574, 2007.

A. Lasaruk and T. Sturm, Effective Quantifier Elimination for Presburger Arithmetic with Infinity, Proc. CASC 2009, vol.5743, pp.195-212, 2009.

D. Lazard, Quantifier Elimination: Optimal Solution for Two Classical Examples, J. Symb. Comput, vol.5, pp.261-266, 1988.

R. Loos and V. Weispfenning, Applying Linear Quantifier Elimination, Comput. J, vol.36, pp.450-462, 1993.

I. Anatolií and . Malcev, Axiomatizable Classes of Locally Free Algebras of Various Types, The Metamathematics of Algebraic Systems. Studies in Logic and the Foundations of Mathematics, vol.66, pp.262-281, 1971.

S. Mccallum, An Improved Projection Operation for Cylindrical Algebraic Decomposition of Three-Dimensional Space, J. Symb. Comput, vol.5, pp.141-161, 1988.

S. Mccallum and H. Hong, On Using Lazard's Projection in CAD Construction, J. Symb. Comput, vol.72, pp.65-81, 2016.

T. S. Motzkin, Beiträge zur Theorie der linearen Ungleichungen. Inaugural Dissertation, 1936.

R. Nieuwenhuis, A. Oliveras, and C. Tinelli, Solving SAT and SAT Modulo Theories: From an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T), J. ACM, vol.53, issue.6, pp.937-977, 2006.

R. Cattamanchi, D. W. Reddy, and . Loveland, Presburger Arithmetic with Bounded Quantifier Alternation, Proc. STOC, pp.320-325, 1978.

J. Renegar, On the Computational Complexity and Geometry of the First-Order Theory of the Reals. Part II, J. Symb. Comput, vol.13, pp.301-328, 1992.

A. M. Seidl and T. Sturm, Boolean Quantification in a FirstOrder Context, Proc. CASC 2003. Institut für Informatik, pp.329-345, 2003.

T. Sturm, Lineare Quantorenelimination in bewerteten Körpern, 1995.

T. Sturm, Real Quantifier Elimination in Geometry. Doctoral Dissertation, 1999.

T. Sturm, Reasoning over Networks by Symbolic, Methods. Appl. Algebr. Eng. Comm, vol.10, pp.79-96, 1999.

T. Sturm, An Algebraic Approach to Offsetting and Blending of Solids, Proc. CASC, pp.367-382, 2000.

T. Sturm, Linear Problems in Valued Fields, J. Symb. Comput, vol.30, pp.207-219, 2000.

T. Sturm, New Domains for Applied Quantifier Elimination, Proc. CASC 2006, vol.4194, pp.295-301, 2006.

T. Sturm, REDLOG Online Resources for Applied Quantifier Elimination, Acta Academiae Aboensis, Ser. B, vol.67, pp.177-191, 2007.

T. Sturm, A Survey of Some Methods for Real Quantifier Elimination, Decision, and Satisfiability and Their Applications, Math. Comput. Sci, vol.11, pp.483-502, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01648690

T. Sturm and A. Tiwari, Verification and Synthesis Using Real Quantifier Elimination, Proc. ISSAC, pp.329-336, 2011.

T. Sturm and A. Weber, Investigating Generic Methods to Solve Hopf Bifurcation Problems in Algebraic Biology, Proc. AB 2008, vol.5147, pp.200-215, 2008.

T. Sturm, A. Weber, O. Essam, M. Abdel-rahman, and . Kahoui, Investigating Algebraic and Logical Algorithms to Solve Hopf Bifurcation Problems in Algebraic Biology, Math. Comput. Sci, vol.2, pp.493-515, 2009.

T. Sturm and V. Weispfenning, Rounding and Blending of Solids by a Real Elimination Method, Proc. IMACS World Congress, vol.2, pp.727-732, 1997.

T. Sturm and V. Weispfenning, Computational Geometry Problems in Redlog, Automated Deduction in Geometry. LNAI, vol.1360, pp.58-86, 1998.
DOI : 10.1007/bfb0022720

T. Sturm and V. Weispfenning, Quantifier Elimination in Term Algebras. The Case of Finite Languages, Proc. CASC 2002. Institut für Informatik, pp.285-300, 2002.

T. Sturm and C. Zengler, Parametric Quantified SAT Solving, Proc. ISSAC 2010. ACM, pp.77-84, 2010.
DOI : 10.1145/1837934.1837954

A. Tarski, The Completeness of Elementary Algebra and Geometry, 1930.

A. Tarski, A Decision Method for Elementary Algebra and Geometry. Prepared for publication by, 1948.
DOI : 10.1007/978-3-7091-9459-1_3
URL : https://babel.hathitrust.org/cgi/imgsrv/download/pdf?id=mdp.39015069248592;orient=0;size=100;seq=5;attachment=0

M. Joachim-von-zur-gathen and . Sieveking, Weitere zum Erfüllungsproblem polynomial äquivalente kombinatorische Aufgaben, Komplexität von Entscheidungsproblemen, vol.43, pp.49-71, 1976.

A. Weber, T. Sturm, and E. O. Abdel-rahman, Algorithmic Global Criteria for Excluding Oscillations, Bull. Math. Biol, vol.73, pp.899-916, 2011.
DOI : 10.1007/s11538-010-9618-0

. Volker-weispfenning, The Complexity of Linear Problems in Fields, J. Symb. Comput, vol.5, pp.3-27, 1988.

. Volker-weispfenning, The Complexity of Almost Linear Diophantine Problems, J. Symb. Comput, vol.10, pp.395-403, 1990.

. Volker-weispfenning, Quantifier Elimination for Real Algebra-the Quadratic Case and Beyond, Appl. Algebr. Eng. Comm, vol.8, pp.85-101, 1997.