M. Abadi and V. Cortier, Deciding knowledge in security protocols under equational theories, Theor. Comput. Sci, vol.367, issue.1-2, pp.2-32, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00000554

M. Adi, Calculs Associatifs-Commutatifs -Etude et réalisation du système UNIFAC, 1991.

M. Adi and C. Kirchner, AC-Unification race: The system solving approach, implementation and benchmarks, J. Symb. Comput, vol.14, issue.1, pp.51-70, 1992.

A. Armando, M. P. Bonacina, S. Ranise, and S. Schulz, New results on rewrite-based satisfiability procedures, ACM Trans. Comput. Log, vol.10, issue.1, p.51, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00576862

A. Armando, S. Ranise, and M. Rusinowitch, A rewriting approach to satisfiability procedures, Inf. Comput, vol.183, issue.2, pp.140-164, 2003.

F. Baader, Combination of compatible reduction orderings that are total on ground terms, Proceedings of the Twelfth Annual IEEE Symposium on Logic in Computer Science (LICS-97), pp.2-13, 1997.

F. Baader and K. Schulz, Combination of constraint solvers for free and quasi-free structures, Theoretical Computer Science, vol.192, pp.107-161, 1998.

F. Baader and K. U. Schulz, Combination techniques and decision problems for disunification, Theoretical Computer Science, vol.142, issue.2, pp.229-255, 1995.

F. Baader, S. Ghilardi, and C. Tinelli, A new combination procedure for the word problem that generalizes fusion decidability results in modal logics, Information & Computation, vol.204, issue.10, pp.1413-1452, 2006.

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.

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

F. Baader and C. Tinelli, Deciding the word problem in the union of equational theories, Information and Computation, vol.178, issue.2, pp.346-390, 2002.

L. Bachmair and H. Ganzinger, Rewrite-based equational theorem proving with selection and simplification, J. Log. Comput, vol.4, issue.3, pp.217-247, 1994.

L. Bachmair, H. Ganzinger, C. Lynch, and W. Snyder, Basic paramodulation, Inf. Comput, vol.121, issue.2, pp.172-192, 1995.

B. Blanchet, Modeling and verifying security protocols with the Applied Pi calculus and proverif, Foundations and Trends in Privacy and Security, vol.1, issue.1-2, pp.1-135, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01423760

M. P. Bonacina, A taxonomy of theorem-proving strategies, Artificial Intelligence Today -Recent Trends and Developments, vol.1600, pp.43-84, 1999.

P. Borovanský, C. Kirchner, H. Kirchner, and P. Moreau, ELAN from a rewriting logic point of view, Theor. Comput. Sci, vol.285, issue.2, pp.155-185, 2002.

A. Boudet, Combining unification algorithms, Journal Symbolic Computation, vol.16, issue.6, pp.597-626, 1993.

M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-oliet et al., All About Maude -A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, Lecture Notes in Computer Science, vol.4350, 2007.

H. Comon, M. Haberstrau, and J. P. Jouannaud, Syntacticness, cycle-syntacticness, and shallow theories, Inf. Comput, vol.111, issue.1, pp.154-191, 1994.

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

E. Domenjoud, F. Klay, and C. Ringeissen, Combination Techniques for Non-disjoint Equational Theories, Proc. of 12th International Conference on Automated Deduction, vol.814, pp.267-281, 1994.

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, Automated Deduction -CADE-24 -24th International Conference on Automated Deduction, vol.7898, pp.249-266, 2013.
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, vol.9322, pp.291-306, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01206669

S. Erbatur, A. M. Marshall, and C. Ringeissen, Notions of knowledge in combinations of theories sharing constructors, Automated Deduction -CADE 26 -26th International Conference on Automated Deduction, vol.10395, pp.60-76, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01587181

S. Escobar, C. Meadows, and J. Meseguer, Maude-NPA: Cryptographic protocol analysis modulo equational properties, Foundations of Security Analysis and Design V, vol.5705, pp.1-50, 2007.

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.

J. P. Jouannaud and C. Kirchner, Solving equations in abstract algebras: a rule-based survey of unification, pp.257-321, 1991.

J. P. Jouannaud and H. Kirchner, Completion of a set of rules modulo a set of equations, SIAM J. Comput, vol.15, issue.4, pp.1155-1194, 1986.

D. Kapur and P. Narendran, Complexity of unification problems with associativecommutative operators, J. Autom. Reasoning, vol.9, issue.2, pp.261-288, 1992.

D. Kapur and P. Narendran, Double-exponential complexity of computing a complete set of AC-unifiers, Proceedings of the Seventh Annual Symposium on Logic in Computer Science (LICS '92), pp.11-21, 1992.

C. Kirchner and F. Klay, Syntactic theories and unification, Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS '90), pp.270-277, 1990.

C. Kirchner and C. Ringeissen, Rule-based constraint programming, Fundam. Inform, vol.34, issue.3, pp.225-262, 1998.
URL : https://hal.archives-ouvertes.fr/inria-00098476

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

S. Meier, B. Schmidt, C. Cremers, and D. A. Basin, The TAMARIN prover for the symbolic analysis of security protocols, Computer Aided Verification -25th International Conference, CAV 2013, vol.8044, pp.696-701, 2013.

J. Meseguer, Variant-based satisfiability in initial algebras, Sci. Comput. Program, vol.154, pp.3-41, 2018.

P. E. Moreau, C. Ringeissen, and M. Vittek, A pattern matching compiler for multiple target languages, Compiler Construction, 12th International Conference, CC 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, vol.2622, pp.61-76, 2003.
URL : https://hal.archives-ouvertes.fr/inria-00099427

G. Nelson and D. C. Oppen, Simplification by cooperating decision procedures, ACM Transations on Programming Languages and Systems, vol.1, issue.2, pp.245-257, 1979.

R. Nieuwenhuis and A. Rubio, Paramodulation-based theorem proving, Handbook of Automated Reasoning, pp.371-443, 2001.

T. Nipkow, Combining matching algorithms: The regular case, Journal of Symbolic Computation, vol.12, issue.6, pp.633-654, 1991.

T. Nipkow, Proof transformations for equational theories, Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS '90), pp.278-288, 1990.

J. Otop, E-unification with constants vs. general E-unification, J. Autom. Reasoning, vol.48, issue.3, pp.363-390, 2012.

D. Pigozzi, The joint of equational theories, Colloquium Mathematicum, pp.15-25, 1974.

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.

C. Ringeissen, Matching with free function symbols -A simple extension of matching?, Rewriting Techniques and Applications, 12th International Conference, RTA, vol.2051, pp.276-290, 2001.
URL : https://hal.archives-ouvertes.fr/inria-00108076

C. Ringeissen, Matching in a class of combined non-disjoint theories, 19th International Conference on Automated Deduction, vol.2741, pp.212-227, 2003.
URL : https://hal.archives-ouvertes.fr/inria-00099610

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

M. Schmidt-schauß, Unification in permutative equational theories is undecidable, J. Symb. Comput, vol.8, issue.4, pp.415-421, 1989.

E. Tidén, Unification in combinations of collapse-free theories with disjoint sets of function symbols, Proc. of the 8th International Conference on Automated Deduction, vol.230, pp.431-449, 1986.

C. Tinelli and C. Ringeissen, Unions of Non-Disjoint Theories and Combinations of Satisfiability Procedures, Theoretical Computer Science, vol.290, issue.1, pp.291-353, 2003.
URL : https://hal.archives-ouvertes.fr/inria-00099668

K. A. Yelick, Unification in combinations of collapse-free regular theories, Journal of Symbolic Computation, vol.3, issue.1/2, pp.153-181, 1987.