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

A. Armando, S. Ranise, and M. Rusinowitch, A rewriting approach to satisfiability procedures, Information and Computation, vol.183, issue.2, pp.140-164, 2003.
DOI : 10.1016/S0890-5401(03)00020-8

F. Baader and S. Ghilardi, Abstract, The Journal of Symbolic Logic, vol.156, issue.02, pp.535-583, 2007.
DOI : 10.1016/j.ic.2005.05.009

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

L. Bachmair and H. Ganzinger, Rewrite-based Equational Theorem Proving with Selection and Simplification, Journal of Logic and Computation, vol.4, issue.3, pp.217-247, 1994.
DOI : 10.1093/logcom/4.3.217

C. Barrett, I. Shikanian, and C. Tinelli, An abstract decision procedure for a theory of inductive data types, JSAT, vol.3, issue.12, pp.21-46, 2007.

P. Baumgartner and U. Waldmann, Hierarchic Superposition with Weak Abstraction, Automated Deduction -CADE-24 -24th International Conference on Automated Deduction, Lake Placid, pp.39-57, 2013.
DOI : 10.1007/978-3-642-38574-2_3
URL : https://hal.archives-ouvertes.fr/hal-00931919

P. Chocron, P. Fontaine, and C. Ringeissen, A Gentle Non-disjoint Combination of Satisfiability Procedures, Proc. of the 7th International Joint Conference on Automated Reasoning, IJCAR, pp.122-136, 2014.
DOI : 10.1007/978-3-319-08587-6_9
URL : https://hal.archives-ouvertes.fr/hal-00985135

P. Chocron, P. Fontaine, and C. Ringeissen, A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited, Proc. Conference on Automated Deduction (CADE), pp.419-433, 2015.
DOI : 10.1007/978-3-319-21401-6_29
URL : https://hal.archives-ouvertes.fr/hal-01157898

P. Fontaine, Combinations of Theories for Decidable Fragments of First-Order Logic, Frontiers of Combining Systems (FroCoS), pp.263-278, 2009.
DOI : 10.1007/s10817-005-5204-9
URL : https://hal.archives-ouvertes.fr/inria-00430631

S. Ghilardi, Model-Theoretic Methods in Combined Constraint Satisfiability, Journal of Automated Reasoning, vol.5, issue.1?2, pp.221-249, 2004.
DOI : 10.1007/s10817-004-6241-5

D. Jovanovic and C. Barrett, Polite Theories Revisited, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'10), pp.402-416, 2010.
DOI : 10.1007/978-3-642-16242-8_29

E. Nicolini, C. Ringeissen, and M. Rusinowitch, Combinable Extensions of Abelian Groups, Proc. Conference on Automated Deduction (CADE), pp.51-66, 2009.
DOI : 10.1006/jsco.2002.0536
URL : https://hal.archives-ouvertes.fr/inria-00428077

E. Nicolini, C. Ringeissen, and M. Rusinowitch, Combining satisfiability procedures for unions of theories with a shared counting operator, Fundam. Inform, vol.105, issue.1 2, pp.163-187, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00526683

S. Ranise, C. Ringeissen, and C. G. Zarba, Combining Data Structures with Nonstably Infinite Theories Using Many-Sorted Logic, Frontiers of Combining Systems (FroCoS), pp.48-64, 2005.
DOI : 10.1007/11559306_3
URL : https://hal.archives-ouvertes.fr/inria-00000570

V. Sofronie-stokkermans, Locality Results for Certain Extensions of Theories with Bridging Functions, Proc. Conference on Automated Deduction (CADE), pp.67-83, 2009.
DOI : 10.1016/j.ic.2006.03.004

V. Sofronie-stokkermans, Automated reasoning in extensions of theories of constructors with recursively defined functions and homomorphisms Interaction versus Automation: The two Faces of Deduction, number 09411 in Dagstuhl Seminar Proceedings. Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, 2010.

P. Suter, M. Dotta, and V. Kuncak, Decision procedures for algebraic data types with abstractions, Principles of Programming Languages (POPL), pp.199-210, 2010.

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.
DOI : 10.1016/S0304-3975(01)00332-2
URL : https://hal.archives-ouvertes.fr/inria-00099668

C. Tinelli and C. G. Zarba, Combining Non-Stably Infinite Theories, Electronic Notes in Theoretical Computer Science, vol.86, issue.1, pp.209-238, 2005.
DOI : 10.1016/S1571-0661(04)80651-0
URL : http://doi.org/10.1016/s1571-0661(04)80651-0

D. Tran, C. Ringeissen, S. Ranise, and H. Kirchner, Combination of convex theories: Modularity, deduction completeness, and explanation, Journal of Symbolic Computation, vol.45, issue.2, pp.261-286, 2010.
DOI : 10.1016/j.jsc.2008.10.006
URL : https://hal.archives-ouvertes.fr/inria-00428583

T. Zhang, H. B. Sipma, and Z. Manna, Decision procedures for term algebras with integer constraints, Information and Computation, vol.204, issue.10, pp.1526-1574, 2006.
DOI : 10.1016/j.ic.2006.03.004
URL : http://doi.org/10.1016/j.ic.2006.03.004