C. Barrett, R. Sebastiani, S. A. Seshia, and C. Tinelli, Satisfiability modulo theories, Handbook of Satisfiability, pp.825-885, 2009.
URL : https://hal.archives-ouvertes.fr/hal-01095009

C. W. Barrett, Checking validity of quantifier-free formulas in combinations of first-order theories, 2003.

D. Barsotti, L. P. Nieto, and A. Tiu, Verification of clock synchronization algorithms: experiments on a combination of deductive tools, Formal Aspects of Computing, vol.144, issue.2, pp.321-341, 2007.
DOI : 10.1007/s00165-007-0027-6
URL : https://hal.archives-ouvertes.fr/inria-00097383

C. W. Brown, QEPCAD B, ACM SIGSAM Bulletin, vol.37, issue.4, pp.97-108, 2003.
DOI : 10.1145/968708.968710

C. W. Brown and J. H. Davenport, The complexity of quantifier elimination and cylindrical algebraic decomposition, Proceedings of the 2007 international symposium on Symbolic and algebraic computation , ISSAC '07, pp.54-60, 2007.
DOI : 10.1145/1277548.1277557

C. W. Brown and M. Kosta, Constructing a single cell in cylindrical algebraic decomposition, Journal of Symbolic Computation, vol.70, pp.14-48, 2015.
DOI : 10.1016/j.jsc.2014.09.024
URL : https://hal.archives-ouvertes.fr/hal-01088452

C. Chen and M. M. Maza, An Incremental Algorithm for Computing Cylindrical Algebraic Decompositions, Computer Mathematics, pp.199-221, 2014.
DOI : 10.1007/978-3-662-43799-5_17

G. E. Collins, Quantifier elimination for real closed fields by cylindrical algebraic decomposition--preliminary report, ACM SIGSAM Bulletin, vol.8, issue.3, pp.80-90, 1974.
DOI : 10.1145/1086837.1086852

G. E. Collins and H. Hong, Partial Cylindrical Algebraic Decomposition for quantifier elimination, Journal of Symbolic Computation, vol.12, issue.3, pp.299-328, 1991.
DOI : 10.1016/S0747-7171(08)80152-6

F. Corzilius, U. Loup, S. Junges, and E. Abraham, SMT-RAT: An SMT-Compliant Nonlinear Real Arithmetic Toolbox, Int. Conf. on Theory and Applications of Satisfiability Testing (SAT'12, pp.442-448, 2011.
DOI : 10.1007/978-3-642-31612-8_35

J. H. Davenport and J. Heintz, Real quantifier elimination is doubly exponential, Journal of Symbolic Computation, vol.5, issue.1-2, pp.29-35, 1988.
DOI : 10.1016/S0747-7171(88)80004-X

L. M. De-moura and N. Bjørner, Model-based Theory Combination, Electronic Notes in Theoretical Computer Science, vol.198, issue.2, pp.37-49, 2008.
DOI : 10.1016/j.entcs.2008.04.079

D. C. De-oliveira, D. Déharbe, and P. Fontaine, Combining decision procedures by (model-)equality propagation, Science of Computer Programming, vol.77, issue.4, pp.518-532, 2012.
DOI : 10.1016/j.scico.2010.04.003
URL : https://hal.archives-ouvertes.fr/inria-00337979

D. Detlefs, G. Nelson, and J. B. Saxe, Simplify: a theorem prover for program checking, Journal of the ACM, vol.52, issue.3, 2003.
DOI : 10.1145/1066100.1066102

A. Dolzmann, Algorithmic strategies for applicable real quantifier elimination, 2000.

A. Dolzmann and T. Sturm, REDLOG, ACM SIGSAM Bulletin, vol.31, issue.2, pp.2-9, 1997.
DOI : 10.1145/261320.261324

A. Dolzmann and T. Sturm, Simplification of Quantifier-free Formulae over Ordered Fields, Journal of Symbolic Computation, vol.24, issue.2, pp.209-231, 1997.
DOI : 10.1006/jsco.1997.0123

A. C. Hearn and R. Schöpf, Reduce User's Manual, Free Version, 2014.

D. Jovanovi´cjovanovi´c and L. De-moura, Solving Non-linear Arithmetic, International Joint Conference on Automated Reasoning (IJCAR), pp.339-354, 2012.
DOI : 10.1007/978-3-642-31365-3_27

T. King, C. Barrett, and C. Tinelli, Leveraging linear and mixed integer programming for SMT, 2014 Formal Methods in Computer-Aided Design (FMCAD), pp.139-163, 2014.
DOI : 10.1109/FMCAD.2014.6987606

M. Kosta, T. Sturm, and A. Dolzmann, Better answers to real questions, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01388720

G. Nelson and D. C. Oppen, Simplification by Cooperating Decision Procedures, ACM Transactions on Programming Languages and Systems, vol.1, issue.2, pp.245-257, 1979.
DOI : 10.1145/357073.357079

A. Tarski, A decision method for elementary algebra and geometry. Rand report. Rand Corporation Republished as A Decision Method for Elementary Algebra and Geometry, 1948.

V. Weispfenning, The complexity of linear problems in fields, Journal of Symbolic Computation, vol.5, issue.1-2, pp.3-27, 1988.
DOI : 10.1016/S0747-7171(88)80003-8

V. Weispfenning, A New Approach to Quantifier Elimination for Real Algebra, 1993.
DOI : 10.1007/978-3-7091-9459-1_20

V. Weispfenning, Quantifier Elimination for Real Algebra -- the Quadratic Case and Beyond, Applicable Algebra in Engineering, Communication and Computing, vol.8, issue.2, pp.85-101, 1993.
DOI : 10.1007/s002000050055

V. Weispfenning, Quantifier elimination for real algebra---the cubic case, Proceedings of the international symposium on Symbolic and algebraic computation , ISSAC '94, pp.258-263, 1994.
DOI : 10.1145/190347.190425