A. Armando, M. P. Bonacina, S. Ranise, and S. Schulz, New results on rewrite-based satisfiability procedures, ACM Transactions on Computational Logic, vol.10, issue.1, 2009.
DOI : 10.1145/1459010.1459014
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 K. U. Schulz, Combination techniques and decision problems for disunification, Theoretical Computer Science, vol.142, issue.2, pp.229-255, 1995.
DOI : 10.1016/0304-3975(94)00277-0

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

T. Bouton, D. C. De-oliveira, D. Déharbe, and P. Fontaine, veriT: An Open, Trustable and Efficient SMT-Solver, Automated Deduction?CADE-22, pp.151-156, 2009.
DOI : 10.1007/978-3-540-73595-3_38
URL : https://hal.archives-ouvertes.fr/inria-00430634

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. Chocron, P. Fontaine, and C. Ringeissen, A Rewriting Approach to the Combination of Data Structures with Bridging Theories, Frontiers of Combining Systems (FroCoS), pp.275-290, 2015.
DOI : 10.1007/978-3-319-24246-0_17
URL : https://hal.archives-ouvertes.fr/hal-01206187

H. Comon, Disunification: A survey, Computational Logic -Essays in Honor of Alan Robinson, pp.322-359, 1991.

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

V. Kuncak, Verifying and Synthesizing Software with Recursive Functions, ICALP, pp.11-25, 2014.
DOI : 10.1007/978-3-662-43948-7_2

J. Meseguer, Variant-based satisfiability in initial algebras Formal Techniques for Safety-Critical Systems -Fourth International Workshop, FTSCS 2015 Communications in Computer and Information Science, vol.596, pp.3-34, 2015.

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

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

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.

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

R. Treinen, A new method for undecidability proofs of first order theories, Journal of Symbolic Computation, vol.14, issue.5, pp.437-458, 1992.
DOI : 10.1016/0747-7171(92)90016-W

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