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.

A. Boudet, Combining Unification Algorithms, Journal of Symbolic Computation, vol.16, issue.6, pp.597-626, 1993.
DOI : 10.1006/jsco.1993.1066

A. Boudet and E. Contejean, On n-syntactic equational theories, Algebraic and Logic Programming, pp.446-457, 1992.
DOI : 10.1007/BFb0013843

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

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, Hierarchical combination of matching algorithms, Twentyeighth International Workshop on Unification (UNIF-2014), 2014.

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.

J. H. Gallier and W. Snyder, Complete sets of transformations for general E-unification, Theoretical Computer Science, vol.67, issue.2-3, pp.203-260, 1989.
DOI : 10.1016/0304-3975(89)90004-2

J. Jouannaud, Syntactic theories, Mathematical Foundations of Computer Science Lecture Notes in Computer Science, vol.452, pp.15-25, 1990.
DOI : 10.1007/BFb0029593

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.

R. Nieuwenhuis, Decidability and Complexity Analysis by Basic Paramodulation, Information and Computation, vol.147, issue.1, pp.1-21, 1998.
DOI : 10.1006/inco.1998.2730

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

T. Nipkow, Combining matching algorithms: The regular case, Journal of Symbolic Computation, vol.12, issue.6, pp.633-654, 1991.
DOI : 10.1016/S0747-7171(08)80145-9

C. Ringeissen, Combining Decision Algorithms for Matching in the Union of Disjoint Equational Theories, Information and Computation, vol.126, issue.2, pp.144-160, 1996.
DOI : 10.1006/inco.1996.0042

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

W. Snyder, A Proof Theory for General Unification, Progress in Computer Science and Applied Logic. Birkhauser, vol.11, 1991.
DOI : 10.1007/978-1-4612-0435-0