C. Areces and P. Fontaine, Combining Theories: The Ackerman and Guarded Fragments, Frontiers of Combining Systems (FroCoS), pp.40-54, 2011.
DOI : 10.1007/978-3-642-04222-5_23

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

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

C. Barrett, R. Sebastiani, S. A. Seshia, and C. Tinelli, Satisfiability modulo theories, Handbook of Satisfiability, pp.825-885, 2009.
URL : https://hal.archives-ouvertes.fr/hal-01095009

M. P. Bonacina, S. Ghilardi, E. Nicolini, S. Ranise, and D. Zucchelli, Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures, International Joint Conference on Automated Reasoning (IJCAR), pp.513-527, 2006.
DOI : 10.1007/11814771_42

E. Börger, E. Grädel, and Y. Gurevich, The Classical Decision Problem. Perspectives in Mathematical Logic, 1997.

B. Dreben and W. D. Goldfarb, The Decision Problem: Solvable Classes of Quantificational Formulas, 1979.

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

H. Ganzinger, C. Meyer, and M. Veanes, The two-variable guarded fragment with transitive relations, Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), pp.24-34, 1999.
DOI : 10.1109/LICS.1999.782582

H. Ganzinger and H. D. Nivelle, A superposition decision procedure for the guarded fragment with equality, Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), pp.295-303, 1999.
DOI : 10.1109/LICS.1999.782624

S. Ghilardi, Model-theoretic methods in combined constraint satisfiability [12] Y. Gurevich and S. Shelah. Spectra of monadic second-order formulas with one unary function, Logic In Computer Science (LICS), pp.3-4221, 2003.

Z. Manna and C. G. Zarba, Combining decision procedures In Formal Methods at the Crossroads . From Panacea to Foundational Support, 10th Anniversary Colloquium of UNU/IIST, Revised Papers, LNCS, vol.2757, pp.381-422, 2003.

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

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.104.2828

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.12, pp.163-187, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00526683

F. P. Ramsey, On a Problem of Formal Logic, Proceedings of the London Mathematical Society, pp.264-286, 1930.

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

C. Ringeissen and V. Senni, Modular Termination and Combinability for Superposition Modulo Counter Arithmetic, Frontiers of Combining Systems (FroCoS), pp.211-226, 2011.
DOI : 10.1007/978-3-642-04222-5_20

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

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, On Combinations of Local Theory Extensions, Programming Logics -Essays in Memory of Harald Ganzinger, pp.392-413, 2013.
DOI : 10.1007/11814771_21

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

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

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.296.7126

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

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.91.4769

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