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

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

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
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. Springer, 2014. Extended version available as Inria Research Report
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), 2015.
DOI : 10.1007/978-3-319-21401-6_29

URL : https://hal.archives-ouvertes.fr/hal-01157898

P. Fontaine, S. Ranise, and C. G. Zarba, Combining Lists with Non-stably Infinite Theories, Logic for Programming, pp.51-66
DOI : 10.1007/978-3-540-32275-7_4

URL : https://hal.archives-ouvertes.fr/inria-00000481

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

G. Nelson and D. C. Oppen, Simplification by Cooperating Decision Procedures, ACM Transactions on Programming Languages and Systems, vol.1, issue.2
DOI : 10.1145/357073.357079

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

T. Pham and M. W. Whalen, An Improved Unrolling-Based Decision Procedure for Algebraic Data Types, Verified Software: Theories, Tools, Experiments -5th International Conference, pp.129-148, 2014.
DOI : 10.1007/978-3-642-54108-7_7

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

R. E. Shostak, A Practical Decision Procedure for Arithmetic with Function Symbols, Journal of the ACM, vol.26, issue.2, pp.351-360, 1979.
DOI : 10.1145/322123.322137

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

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

P. Suter, A. S. Köksal, and V. Kuncak, Satisfiability Modulo Recursive Programs, Static Analysis -18th International Symposium, SAS 2011, pp.298-315, 2011.
DOI : 10.1007/978-3-540-77395-5_17

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.
DOI : 10.1007/978-94-009-0349-4_5

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

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. Wies, R. Piskac, and V. Kuncak, Combining Theories with Shared Set Operations, Frontiers of Combining Systems (FroCoS), pp.366-382, 2009.
DOI : 10.1016/S0304-3975(01)00332-2

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

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

C. G. Zarba, Combining Sets with Cardinals, Journal of Automated Reasoning, vol.9, issue.59, pp.1-29, 2005.
DOI : 10.1007/s10817-005-3075-8

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

V. Note, V. Struct, V. Elem, and V. Elem, We are now ready to define an interpretation M. First, we specify the domains . Let M t = B t for any sort t ? ? t and M s = A s for any s ? ? s . Hence M struct is T struct (? s ? V )/ = E . We consider the following interpretation in M: ? for