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

F. Baader and K. U. Schulz, Unification in the union of disjoint equational theories: Combining decision procedures, Journal of Symbolic Computation, vol.21, issue.2, pp.211-243, 1996.

H. Comon-lundh and S. Delaune, The finite variant property: How to get rid of some algebraic properties, Rewriting Techniques and Applications, vol.3467, pp.294-307, 2005.

A. K. Eeralla, S. Erbatur, A. M. Marshall, and C. Ringeissen, Rule-based unification in combined theories and the finite variant property, Language and Automata Theory and Applications -13th International Conference, vol.11417, pp.356-367, 2019.
URL : https://hal.archives-ouvertes.fr/hal-01988419

S. Erbatur, D. Kapur, A. M. Marshall, P. Narendran, and C. Ringeissen, Hierarchical combination, 24 -24th International Conference on Automated Deduction, vol.7898, pp.249-266, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00878649

S. Erbatur, A. M. Marshall, D. Kapur, and P. Narendran, Unification over distributive exponentiation (sub)theories, Journal of Automata, Languages and Combinatorics (JALC), vol.16, issue.2-4, pp.109-140, 2011.

S. Escobar, R. Sasse, and J. Meseguer, Folding variant narrowing and optimal variant termination, J. Log. Algebr. Program, vol.81, issue.7-8, pp.898-928, 2012.

D. Kim, C. Lynch, and P. Narendran, Reviving basic narrowing modulo, Frontiers of Combining Systems -12th International Symposium, vol.11715, pp.313-329, 2019.

C. Lynch and B. Morawska, Automated Deduction -CADE-18, 18th International Conference on Automated Deduction, vol.2392, pp.471-485, 2002.

M. Schmidt-schauß, Unification in a combination of arbitrary disjoint equational theories, Journal of Symbolic Computation, vol.8, pp.51-99, 1989.

E. Tidén and S. Arnborg, Unification problems with one-sided distributivity, Journal of Symbolic Computation, vol.3, issue.1, pp.183-202, 1987.