F. Baader and J. H. Siekmann, Unification theory, Handbook of Logic in Artificial Intelligence and Logic Programming, Volume2, Deduction Methodologies, pp.41-126, 1994.

P. Backeman and P. Rümmer, Theorem Proving with Bounded Rigid E-Unification
DOI : 10.1007/978-3-319-21401-6_39

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

P. Baumgartner, J. Bax, and U. Waldmann, Finite Quantification in Hierarchic Theorem Proving, Automated Reasoning, pp.152-167
DOI : 10.1007/978-3-319-08587-6_11
URL : https://hal.archives-ouvertes.fr/hal-01087873

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, 2009.
DOI : 10.1007/978-3-540-73595-3_38
URL : https://hal.archives-ouvertes.fr/inria-00430634

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

Y. Ge and L. De-moura, Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories, LNCS, vol.5643, pp.306-320, 2009.
DOI : 10.1007/978-3-642-02658-4_25

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

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.

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

A. Reynolds, C. Tinelli, and L. M. 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. Tiwari, L. Bachmair, and H. Rueß, Rigid E-Unification Revisited, Lecture Notes in Artificial Intelligence, vol.1831, pp.220-234, 2000.
DOI : 10.1007/10721959_17