F. Baader and T. Nipkow, Term Rewriting and All That, 1998.

F. Baader and W. Snyder, Unification Theory, Handbook of Automated Reasoning, 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

P. Backeman and P. Rümmer, Efficient Algorithms for Bounded Rigid E-unification, Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX), pp.70-85, 2015.
DOI : 10.1007/10721959_17

P. Backeman and P. Rümmer, Theorem Proving with Bounded Rigid E-Unification, Proc. Conference on Automated Deduction (CADE), volume 9195 of Lecture Notes in Computer Science, 2015.
DOI : 10.1007/978-3-319-21401-6_39

H. Barbosa, P. Fontaine, and A. Reynolds, Congruence Closure with Free Variables
DOI : 10.1007/10721959_17

URL : https://hal.archives-ouvertes.fr/hal-01442691

C. Barrett, R. Sebastiani, S. 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 SMT-LIB Standard: Version 2.0, International Workshop on Satisfiability Modulo Theories (SMT), 2010.
DOI : 10.1007/978-3-642-19583-9_2

B. Beckert, Ridig E-Unification Automated Deduction: A Basis for Applications, Foundations: Calculi and Methods, vol.1, 1998.

T. Bouton, D. C. De-oliveira, D. Déharbe, and P. Fontaine, veriT: An Open, Trustable and Efficient SMT-Solver, Proc. Conference on Automated Deduction (CADE), 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, Proc. Conference on Automated Deduction, pp.183-198, 2007.
DOI : 10.1007/978-3-540-73595-3_13

L. De-moura and N. Bjørner, Engineering DPLL(T) + Saturation, International Joint Conference on Automated Reasoning (IJCAR), pp.475-490, 2008.
DOI : 10.1007/978-3-540-71070-7_40

L. M. De-moura and N. Bjørner, Z3: An Efficient SMT Solver, Tools and Algorithms for Construction and Analysis of Systems (TACAS), pp.337-340, 2008.
DOI : 10.1007/978-3-540-78800-3_24

A. Degtyarev and A. Voronkov, Equality Reasoning in Sequent-Based Calculi, Handbook of Automated Reasoning, pp.611-706, 2001.
DOI : 10.1016/B978-044450813-3/50012-6

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.11.5202

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

URL : http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.70.1745&rep=rep1&type=pdf

M. Fitting, First-Order Logic and Automated Theorem Proving, 1990.
DOI : 10.1007/978-1-4612-2360-3

Y. Ge and L. De-moura, Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories, Computer Aided Verification (CAV), pp.306-320, 2009.
DOI : 10.1007/978-3-540-78800-3_19

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.150.833

J. Goubault, A rule-based algorithm for rigid E-unification, Computational Logic and Proof Theory: Third Kurt Gödel Colloquium, KGC'93, pp.202-210, 1993.
DOI : 10.1007/BFb0022569

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.40.5053

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

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.125.3226

R. Nieuwenhuis and A. Oliveras, Fast congruence closure and extensions. Information and Computation, Special Issue: 16th International Conference on Rewriting Techniques and Applications, pp.557-580, 2007.
DOI : 10.1016/j.ic.2006.08.009

URL : http://doi.org/10.1016/j.ic.2006.08.009

R. Piskac, T. Wies, and D. Zufferey, GRASShopper, Tools and Algorithms for Construction and Analysis of Systems (TACAS), pp.124-139, 2014.
DOI : 10.1007/978-3-642-54862-8_9

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.195-202, 2014.
DOI : 10.1109/FMCAD.2014.6987613

A. Reynolds, C. Tinelli, A. Goel, S. Krsti´ckrsti´c, M. Deters et al., Quantifier Instantiation Techniques for Finite Model Finding in SMT, Proc. Conference on Automated Deduction (CADE), pp.377-391, 2013.
DOI : 10.1007/978-3-642-38574-2_26

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.567.7320

P. Rümmer, E-Matching with Free Variables, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), pp.359-374, 2012.
DOI : 10.1007/978-3-642-28717-6_28

A. Tiwari, L. Bachmair, and H. Ruess, Rigid E-Unification Revisited, Proc. Conference on Automated Deduction (CADE), volume 1831 of Lecture Notes in Computer Science, pp.220-234, 2000.
DOI : 10.1007/10721959_17

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.36.7046