F. Baader and T. Nipkow, Term rewriting and all that, 1998.

C. Bouchard, K. A. Gero, C. Lynch, and P. Narendran, On Forward Closure and the Finite Variant Property, Frontiers of Combining Systems, pp.327-342, 2013.
DOI : 10.1007/978-3-642-40885-4_23
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.431.2441

H. Comon, M. Haberstrau, and J. Jouannaud, Syntacticness, Cycle-Syntacticness, and Shallow Theories, Information and Computation, vol.111, issue.1, pp.154-191, 1994.
DOI : 10.1006/inco.1994.1043
URL : http://doi.org/10.1006/inco.1994.1043

H. Comon-lundh and S. Delaune, The Finite Variant Property: How to Get Rid of Some Algebraic Properties, Rewriting Techniques and Applications, pp.294-307, 2005.
DOI : 10.1007/978-3-540-32033-3_22

S. ¸tefan-ciobâc?-a, S. Delaune, and S. Kremer, Computing knowledge in security protocols under convergent equational theories, J. Autom. Reasoning, vol.48, issue.2, pp.219-262, 2012.

E. Domenjoud, F. Klay, and C. Ringeissen, Combination techniques for non-disjoint equational theories, International Conference on Automated Deduction, pp.267-281, 1994.
DOI : 10.1007/3-540-58156-1_19
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.54.8167

S. Erbatur, D. Kapur, A. M. Marshall, P. Narendran, and C. Ringeissen, Hierarchical Combination, Automated Deduction (CADE-24), pp.249-266, 2013.
DOI : 10.1007/978-3-642-38574-2_17
URL : https://hal.archives-ouvertes.fr/hal-00878649

S. Erbatur, D. Kapur, A. M. Marshall, P. Narendran, and C. Ringeissen, Unification and Matching in Hierarchical Combinations of Syntactic Theories, Frontiers of Combining Systems -10th International Symposium Proceedings, volume 9322 of Lecture Notes in Computer Science, pp.291-306, 2015.
DOI : 10.1016/S0747-7171(89)80022-7
URL : https://hal.archives-ouvertes.fr/hal-01206669

S. Erbatur, A. M. Marshall, and C. Ringeissen, Unification in non-disjoint combinations with forward-closed theories. Available at https

S. Escobar, R. Sasse, and J. Meseguer, Folding variant narrowing and optimal variant termination, The Journal of Logic and Algebraic Programming, vol.81, issue.7-8, pp.898-928, 2012.
DOI : 10.1016/j.jlap.2012.01.002
URL : http://doi.org/10.1016/j.jlap.2012.01.002

J. Jouannaud and C. Kirchner, Solving equations in abstract algebras: A rule-based survey of unification, Computational Logic -Essays in Honor of Alan Robinson, pp.257-321, 1991.

C. Kirchner and F. Klay, Syntactic theories and unification, [1990] Proceedings. Fifth Annual IEEE Symposium on Logic in Computer Science, pp.270-277, 1990.
DOI : 10.1109/LICS.1990.113753

C. Lynch and B. Morawska, Basic syntactic mutation Automated Deduction -CADE-18, 18th International Conference on Automated Deduction Proceedings, volume 2392 of Lecture Notes in Computer Science, pp.471-485, 2002.

T. Nipkow, Proof transformations for equational theories, [1990] Proceedings. Fifth Annual IEEE Symposium on Logic in Computer Science, pp.278-288, 1990.
DOI : 10.1109/LICS.1990.113754

C. Ringeissen, Unification in a combination of equational theories with shared constants and its application to primal algebras, The 1st International Conference on Logic Programming and Automated Reasoning, pp.261-272, 1992.
DOI : 10.1007/BFb0013067

M. Schmidt-schauß, Unification in a combination of arbitrary disjoint equational theories, Journal of Symbolic Computation, vol.8, issue.1-2, pp.51-99, 1989.
DOI : 10.1016/S0747-7171(89)80022-7

K. A. Yelick, Unification in combinations of collapse-free regular theories, Journal of Symbolic Computation, vol.3, issue.1-2, pp.153-181, 1987.
DOI : 10.1016/S0747-7171(87)80025-1