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

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

M. P. Bonacina and M. Echenim, T-decision by decomposition, Proc. of the 21st Int. Conf. on Automated Deduction (CADE), volume 4603 of LNAI, pp.199-214, 2007.

M. P. Bonacina and M. Echenim, On Variable-inactivity and Polynomial Formula-Satisfiability Procedures, Journal of Logic and Computation, vol.18, issue.1, pp.77-96, 2008.
DOI : 10.1093/logcom/exm055

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

M. Bozzano, R. Bruttomesso, A. Cimatti, T. A. Junttila, S. Ranise et al., Efficient theory combination via boolean search, Information and Computation, vol.204, issue.10, pp.1493-1525, 2006.
DOI : 10.1016/j.ic.2005.05.011

A. Bradley and Z. Manna, The Calculus of Computation, 2007.

A. R. Bradley, Z. Manna, and H. B. Sipma, What???s Decidable About Arrays?, Proc. of the 7th Int. Conf. on Verification, Model Checking, and Abstract Interpretation (VM- CAI 2006), pp.427-442, 2006.
DOI : 10.1007/11609773_28

R. E. Bryant, S. K. Lahiri, and S. A. Seshia, Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions, Proc. of CAV 2002, pp.78-92, 2002.
DOI : 10.1007/3-540-45657-0_7

H. B. Enderton, A Mathematical Introduction to Logic, 1972.

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

S. Ghilardi, E. Nicolini, S. Ranise, and D. Zucchelli, Noetherianity and Combination Problems
DOI : 10.1007/978-3-540-74621-8_14
URL : https://hal.archives-ouvertes.fr/inria-00576594

S. Ghilardi, E. Nicolini, and D. Zucchelli, A comprehensive combination framework, ACM Transactions on Computational Logic, vol.9, issue.2, pp.1-54, 2008.
DOI : 10.1145/1342991.1342992
URL : https://hal.archives-ouvertes.fr/inria-00576602

C. Ihlemann, S. Jacobs, and V. Sofronie-stokkermans, On Local Reasoning in Verification, Proc. of TACAS 2008, pp.265-281, 2008.
DOI : 10.1007/978-3-540-78800-3_19

H. Kirchner, S. Ranise, C. Ringeissen, and D. Tran, On superpositionbased satisfiability procedures and their combination, Proc. of IC- TAC 2005, pp.594-608, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00000586

S. Krsti´ckrsti´c, A. Goel, J. Grundy, and C. Tinelli, Combined satisfiability modulo parametric theories, Proc. of TACAS, pp.618-631, 2007.

C. Lynch and B. Morawska, Automatic decidability, Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, p.7, 2002.
DOI : 10.1109/LICS.2002.1029813
URL : https://hal.archives-ouvertes.fr/inria-00586936

C. Lynch and D. Tran, Automatic Decidability and Combinability Revisited, Proc. of CADE-21, pp.328-344, 2007.
DOI : 10.1007/978-3-540-73595-3_22
URL : https://hal.archives-ouvertes.fr/inria-00576605

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

R. Nieuwenhuis and A. Rubio, Paramodulation-Based Theorem Proving, Handbook of Automated Reasoning, volume I, chapter 7, pp.371-443, 2001.
DOI : 10.1016/B978-044450813-3/50009-6

R. E. Shostak, Deciding Combinations of Theories, Journal of the ACM, vol.31, issue.1, pp.1-12, 1984.
DOI : 10.1145/2422.322411

D. Zucchelli, Combination Methods for Software Verification INRIA Centre de recherche INRIA Nancy ? Grand Est LORIA, Technopôle de Nancy-Brabois -Campus scientifique 615, rue du Jardin Botanique -BP 101 -54602 Villers-lès, 2008.