F. Baader and W. Snyder, Unification theory, Handbook of Automated Reasoning (in 2 volumes), pp.445-532, 2001.

L. Bachmair and H. Ganzinger, Rewrite-based Equational Theorem Proving with Selection and Simplification, Journal of Logic and Computation, vol.4, issue.3, pp.217-247, 1994.
DOI : 10.1093/logcom/4.3.217

C. Barrett, R. Sebastiani, S. Seshia, and C. Tinelli, Satisfiability Modulo Theories
URL : https://hal.archives-ouvertes.fr/hal-01095009

C. Barrett, A. Stump, and C. Tinelli, The SMT-LIB Standard: Version 2.0, Proceedings of the 8th International Workshop on Satisfiability Modulo Theories, 2010.

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

L. De-moura and N. Bjørner, Efficient E-Matching for SMT Solvers, Automated Deduction CADE-21, pp.183-198, 2007.
DOI : 10.1007/978-3-540-73595-3_13

L. M. De-moura and N. Bjørner, Z3: An Efficient SMT Solver In Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software. Proceedings, pp.337-340, 2008.

D. Déharbe, P. Fontaine, D. L. Berre, and B. Mazure, Computing prime implicants, 2013 Formal Methods in Computer-Aided Design, pp.46-52, 2013.
DOI : 10.1109/FMCAD.2013.6679390

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

Y. Ge, C. Barrett, and C. Tinelli, Solving Quantified Verification Conditions Using Satisfiability Modulo Theories, Automated Deduction CADE-21, pp.167-182, 2007.
DOI : 10.1007/978-3-540-73595-3_12

K. R. Leino, M. Musuvathi, and X. Ou, A Two-Tier Technique for Supporting Quantifiers in a Lazily Proof-Explicating Theorem Prover, Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS'05, pp.334-348, 2005.
DOI : 10.1007/978-3-540-31980-1_22

L. Moura and N. Bjørner, Engineering DPLL(T) + Saturation, Proceedings of the 4th International Joint Conference on Automated Reasoning, IJCAR '08, pp.475-490, 2008.
DOI : 10.1007/978-3-540-71070-7_40

G. Nelson and D. C. Oppen, Fast Decision Procedures Based on Congruence Closure, Journal of the ACM, vol.27, issue.2, pp.356-364, 1980.
DOI : 10.1145/322186.322198

R. Nieuwenhuis and A. Oliveras, Fast congruence closure and extensions. Information and Computation, Special Issue: 16th International Conference on Rewriting Techniques and Applica- tions, pp.557-580, 2007.

R. Nieuwenhuis and A. Rubio, Paramodulation-Based Theorem Proving, Handbook of automated reasoning, pp.371-443, 2001.
DOI : 10.1016/B978-044450813-3/50009-6

J. Otten, Restricting backtracking in connection calculi, AI Commun, vol.23, issue.2-3, pp.159-182, 2010.

G. Reger, D. Tishkovsky, and A. Voronkov, Cooperating Proof Attempts, Automated Deduction - CADE-25 -25th International Conference on Automated Deduction Proceedings, pp.339-355, 2015.
DOI : 10.1007/978-3-319-21401-6_23

A. Reynolds, C. Tinelli, and L. De-moura, Finding conflicting instances of quantified formulas in SMT, 2014 Formal Methods in Computer-Aided Design (FMCAD), pp.31195-31202, 2014.
DOI : 10.1109/FMCAD.2014.6987613

A. Tiwari, L. Bachmair, and H. Ruess, Rigid E-Unification Revisited, Lecture Notes in Computer Science, vol.17, issue.1831, pp.220-234, 2000.
DOI : 10.1007/10721959_17