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.
DOI : 10.1006/jsco.1996.0009

F. Baader and W. Snyder, Unification theory, Handbook of Automated Reasoning, pp.445-532, 2001.

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

S. Erbatur, D. Kapur, A. M. Marshall, P. Narendran, and C. Ringeissen, Hierarchical Combination, Proceedings of 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, A. M. Marshall, D. Kapur, and P. Narendran, Unification over distributive exponentiation (sub)theories, Journal of Automata, Languages and Combinatorics (JALC), vol.16, pp.2-4109, 2011.

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