J. Abbott, A. M. Bigatti, and G. E. Lagorio, CoCoA-5: A system for doing computations in commutative algebra Building bridges between symbolic computation and satisfiability checking, Proceedings ISSAC 2015, pp.1-6, 2015.

N. H. Arai, T. Matsuzaki, H. Iwane, and H. Anai, Mathematics by machine, Proceedings of the 39th International Symposium on Symbolic and Algebraic Computation, ISSAC '14, pp.1-8, 2014.
DOI : 10.1145/2608628.2627488

C. Barrett, D. Kroening, and T. Melham, Problem solving for the 21st century: Efficient solvers for satisfiability modulo theories, and Smith Institute for Industrial Mathematics and System Engineering, 2014.

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. Barrett, A. Stump, and C. Tinelli, The satisfiability modulo theories library (SMT- LIB ). www, 2010.

R. E. Bixby, Computational progress in linear and mixed integer programming. Presentation at ICIAM, p.2015, 2015.

F. Bobot, S. Conchon, E. Contejean, A. Mahboubi, A. Mebsout et al., A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic, Proceedings IJCAR 2012, pp.67-81, 2012.
DOI : 10.1007/978-3-642-31365-3_8
URL : https://hal.archives-ouvertes.fr/hal-00687640

C. Borralleras, S. Lucas, R. Navarro-marset, E. Rodriguez-carbonell, and A. Rubio, Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic, Proceedings CADE-22, pp.294-305, 2009.
DOI : 10.1007/11562931_24

W. Bosma, J. Cannon, and C. Playoust, The Magma Algebra System I: The User Language, Journal of Symbolic Computation, vol.24, issue.3-4, pp.235-265, 1993.
DOI : 10.1006/jsco.1996.0125

T. Bouton, D. Caminha, B. De-oliveira, D. Déharbe, and P. Fontaine, veriT: An Open, Trustable and Efficient SMT-Solver, Proceedings CADE-22, pp.151-156, 2009.
DOI : 10.1007/978-3-540-73595-3_38
URL : https://hal.archives-ouvertes.fr/inria-00430634

R. J. Bradford, C. Chen, J. H. Davenport, M. England, M. Moreno-maza et al., Truth Table Invariant Cylindrical Algebraic Decomposition by Regular Chains, Proceedings CASC 2014, pp.44-58, 2014.
DOI : 10.1007/978-3-319-10515-4_4

R. Bradford, J. Davenport, M. England, S. Mccallum, and D. Wilson, Truth table invariant cylindrical algebraic decomposition, Journal of Symbolic Computation, vol.76, pp.1-35, 2016.
DOI : 10.1016/j.jsc.2015.11.002
URL : http://doi.org/10.1016/j.jsc.2015.11.002

M. Bromberger, T. Sturm, and C. Weidenbach, Linear Integer Arithmetic Revisited, Proceedings CADE-25, pp.623-637, 2015.
DOI : 10.1007/978-3-319-21401-6_42
URL : https://hal.archives-ouvertes.fr/hal-01239394

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

R. Bruttomesso, E. Pek, N. Sharygina, and A. Tsitovich, The OpenSMT2 solver, Proceedings TACAS 2010, pp.150-153, 2010.

B. Buchberger, Ein Algorithmus zum Auffinden des basiselemente des Restklassenringes nach einem nulldimensionalen Polynomideal, english translation: J. Symbolic Computation, pp.475-511, 1965.

C. Chen, M. Moreno-maza, B. Xia, and L. Yang, Computing cylindrical algebraic decomposition via triangular decomposition, Proceedings of the 2009 international symposium on Symbolic and algebraic computation, ISSAC '09, pp.95-102, 2009.
DOI : 10.1145/1576702.1576718

A. Cimatti, A. Griggio, B. Schaafsma, and R. Sebastiani, The MathSAT5 SMT Solver, Proceedings TACAS 2013, pp.93-107, 2013.
DOI : 10.1007/978-3-642-36742-7_7

M. Codish, Y. Fekete, C. Fuhs, J. Giesl, and J. Waldmann, Exotic semi-ring constraints, Proceedings SMT 2013. EPiC Series, pp.88-97, 2013.

G. E. Collins, The SAC-1 system, Proceedings of the second ACM symposium on Symbolic and algebraic manipulation , SYMSAC '71, pp.144-152, 1971.
DOI : 10.1145/800204.806279

G. E. Collins, Quantifier elimination for real closed fields by cylindrical algebraic decomposition, Automata Theory and Formal Languages, pp.134-183, 1975.

S. Conchon, M. Iguernelala, and A. Mebsout, A collaborative framework for nonlinear integer arithmetic reasoning in Alt-Ergo, Proceedings SYNASC 2013, pp.161-168, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00924646

S. A. Cook, The complexity of theorem-proving procedures, Proceedings of the third annual ACM symposium on Theory of computing , STOC '71, pp.151-158, 1971.
DOI : 10.1145/800157.805047

F. Corzilius, G. Kremer, S. Junges, S. Schupp, and E. Abrahám, SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving, Proc. SAT 2015, pp.360-368, 2015.
DOI : 10.1007/978-3-319-24318-4_26

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

M. Davis, G. Logemann, and D. Loveland, A machine program for theorem-proving, Communications of the ACM, vol.5, issue.7, pp.394-397, 1962.
DOI : 10.1145/368273.368557

M. Davis and H. Putnam, A Computing Procedure for Quantification Theory, Journal of the ACM, vol.7, issue.3, pp.201-215, 1960.
DOI : 10.1145/321033.321034

W. Decker, G. M. Greuel, G. Pfister, and H. Schönemann, Singular 4-0-2 ? A computer algebra system for polynomial computations, 2015.

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

B. Dutertre and L. De-moura, A Fast Linear-Arithmetic Solver for DPLL(T), Proc. CAV 2006, pp.81-94, 2006.
DOI : 10.1007/11817963_11

M. Era¸scuera¸scu and H. Hong, Synthesis of optimal numerical algorithms using real quantifier elimination (Case study: Square root computation), Proceedings ISSAC 2014, pp.162-169, 2014.

M. Fränzle, C. Herde, T. Teige, S. Ratschan, and T. Schubert, Efficient solving of large non-linear arithmetic constraint systems with complex Boolean structure, Journal on Satisfiability Boolean Modeling and Computation, vol.1, pp.3-4, 2007.

D. R. Grayson and M. E. Stillman, Macaulay2, a software system for research in algebraic geometry

A. C. Hearn, REDUCE: The first forty years, Proceedings A3L. pp. 19?24. Books on Demand GmbH, 2005.

R. D. Jenks and R. S. Sutor, AXIOM: The Scientific Computation System, 1992.

D. Jovanovi´cjovanovi´c and L. De-moura, Solving non-linear arithmetic, Proceedings IJCAR 2012. LNAI, pp.339-354, 2012.

H. G. Kahrimanian, Analytic Differentiation by a Digital Computer, 1953.

D. Kroening and O. Strichman, Decision Procedures: An Algorithmic Point of View, 2008.
DOI : 10.1007/978-3-662-50497-0

J. P. Marques-silva and K. A. Sakallah, GRASP: a search algorithm for propositional satisfiability, IEEE Transactions on Computers, vol.48, issue.5, pp.506-521, 1999.
DOI : 10.1109/12.769433

W. A. Martin and R. J. Fateman, The MACSYMA system, Proceedings of the second ACM symposium on Symbolic and algebraic manipulation , SYMSAC '71, pp.59-75, 1971.
DOI : 10.1145/800204.806267

J. Moses, Symbolic Integration, p.47, 1967.

L. De-moura and G. O. Passmore, The Strategy Challenge in SMT Solving, In: Automated Reasoning and Mathematics, vol.12, issue.2, pp.15-44, 2013.
DOI : 10.1007/978-3-642-17511-4_27

L. M. De-moura and N. Bjørner, Z3: An Efficient SMT Solver, Proceedings TACAS 2008, pp.337-340, 2008.
DOI : 10.1007/978-3-540-78800-3_24

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

J. Nolan, Analytic Differentiation on a Digital Computer. Master's thesis, M.I.T, 1953.

A. Platzer, J. D. Quesel, and P. Rümmer, Real World Verification, Proceedings CADE-22, pp.485-501, 2009.
DOI : 10.1007/978-3-540-70545-1_17

R. H. Risch, The problem of integration in finite terms, Transactions of the American Mathematical Society, vol.139, pp.167-189, 1969.
DOI : 10.1090/S0002-9947-1969-0237477-8

K. Scheibler, S. Kupferschmid, and B. Becker, Recent improvements in the SMT solver iSAT, Proceedings MBMV 2013 Institut für Angewandte Mikroelektronik und Datentechnik, Fakultät für Informatik und Elektrotechnik, pp.231-241, 2013.

J. Slagle, A Heuristic Program that Solves Symbolic Integration Problems in Freshman Calculus, Journal of the ACM, vol.10, issue.4, 1961.
DOI : 10.1145/321186.321193

A. Strzebo´nskistrzebo´nski, Solving polynomial systems over semialgebraic sets represented by cylindrical algebraic formulas, Proceedings ISSAC'12, pp.335-342, 2012.

V. Weispfenning, Comprehensive Gr??bner bases, Journal of Symbolic Computation, vol.14, issue.1, pp.1-29, 1992.
DOI : 10.1016/0747-7171(92)90023-W

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, 1997.

W. Research and . Inc, Mathematica, version 10.4, 2016.

H. Zankl and A. Middeldorp, Satisfiability of Non-linear (Ir)rational??Arithmetic, Proceedings LPAR 2010. LNAI, pp.481-500, 2010.
DOI : 10.1007/978-3-642-17511-4_27