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, Inf. Comput, vol.183, issue.2, pp.140-164, 2003.

F. Baader and S. Ghilardi, Connecting many-sorted theories, J. Symb. Log, vol.72, issue.2, pp.535-583, 2007.

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, J. Log. Comput, vol.4, issue.3, pp.217-247, 1994.

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

P. Baumgartner and U. Waldmann, Hierarchic superposition with weak abstraction, Automated Deduction -CADE-24 -24th International Conference on Automated Deduction, vol.7898, pp.39-57, 2013.
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, vol.8562, pp.122-136, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01087162

P. Chocron, P. Fontaine, and C. Ringeissen, A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited, Automated Deduction -CADE-25 -25th International Conference on Automated Deduction, vol.9195, pp.419-433, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01157898

P. Chocron, P. Fontaine, and C. Ringeissen, A rewriting approach to the combination of data structures with bridging theories, Frontiers of Combining Systems (FroCoS), vol.9322, pp.275-290, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01206187

P. Fontaine, S. Ranise, and C. G. Zarba, Combining lists with non-stably infinite theories, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'04), vol.3452, pp.51-66, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00000481

S. Ghilardi, Model-theoretic methods in combined constraint satisfiability, Journal of Automated Reasoning, vol.33, issue.3-4, pp.221-249, 2004.

D. Jovanovic and C. Barrett, Polite theories revisited, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'10), vol.6397, pp.402-416

. Springer, , 2010.

E. Kruglov and C. Weidenbach, Superposition decides the first-order logic fragment over ground theories, Mathematics in Computer Science, vol.6, issue.4, pp.427-456, 2012.

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

E. Nicolini, C. Ringeissen, and M. Rusinowitch, Combinable extensions of Abelian groups, 22nd International Conference on Automated Deduction, vol.5663, pp.51-66, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00383041

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

D. C. Oppen, Reasoning about recursively defined data structures, J. ACM, vol.27, issue.3, pp.403-411, 1980.

T. Pham, A. Gacek, and M. W. Whalen, Reasoning about algebraic data types with abstractions, J. Autom. Reasoning, vol.57, issue.4, pp.281-318, 2016.

S. Ranise, C. Ringeissen, and C. G. Zarba, Combining data structures with nonstably infinite theories using many-sorted logic, Frontiers of Combining Systems (FroCoS), vol.3717, pp.48-64, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00070335

R. E. Shostak, A practical decision procedure for arithmetic with function symbols, J. ACM, vol.26, issue.2, pp.351-360, 1979.

V. Sofronie-stokkermans, Locality results for certain extensions of theories with bridging functions, 22nd International Conference on Automated Deduction, vol.5663, pp.67-83, 2009.

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.

P. Suter, A. S. Köksal, and V. Kuncak, Satisfiability modulo recursive programs, Static Analysis -18th International Symposium, vol.6887, pp.298-315, 2011.

C. Tinelli, Cooperation of background reasoners in theory reasoning by residue sharing, J. Autom. Reasoning, vol.30, issue.1, pp.1-31, 2003.

C. Tinelli and M. T. Harandi, A new correctness proof of the Nelson-Oppen combination procedure, Frontiers of Combining Systems (FroCoS), Applied Logic, pp.103-120, 1996.

C. Tinelli and C. Ringeissen, Unions of non-disjoint theories and combinations of satisfiability procedures, Theoretical Comput. Sci, vol.290, issue.1, pp.291-353, 2003.
URL : https://hal.archives-ouvertes.fr/inria-00099668

D. Tran, C. Ringeissen, S. Ranise, and H. Kirchner, Combination of convex theories: Modularity, deduction completeness, and explanation, J. Symb. Comput, vol.45, issue.2, pp.261-286, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00331479

T. Wies, R. Piskac, and V. Kuncak, Combining theories with shared set operations, Frontiers of Combining Systems, vol.5749, pp.366-382, 2009.

C. G. Zarba, Combining lists with integers, International Joint Conference on Automated Reasoning (Short Papers), pp.170-179, 2001.

C. G. Zarba, Combining multisets with integers, 18th International Conference on Automated Deduction, vol.2392, pp.363-376, 2002.

C. G. Zarba, Combining sets with cardinals, J. Autom. Reasoning, vol.34, issue.1, pp.1-29, 2005.

T. Zhang, H. B. Sipma, and Z. Manna, Decision procedures for term algebras with integer constraints, Inf. Comput, vol.204, issue.10, pp.1526-1574, 2006.