A. Armando, M. 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, 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

B. Buchberger, A theoretical basis for the reduction of polynomials to canonical forms, ACM SIGSAM Bulletin, vol.10, issue.3, pp.19-29, 1976.
DOI : 10.1145/1088216.1088219

L. M. De-moura and N. Bjørner, Engineering DPLL(T) + Saturation, Proc. of IJCAR '08, pp.475-490, 2008.
DOI : 10.1007/978-3-540-71070-7_40

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, 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

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

J. Lassez and M. J. Maher, On Fourier's algorithm for linear arithmetic constraints, Journal of Automated Reasoning, vol.38, issue.3, pp.373-379, 1992.
DOI : 10.1007/BF00245296

J. Lassez and K. Mcaloon, A canonical form for generalized linear constraints, Journal of Symbolic Computation, vol.13, issue.1, pp.1-24, 1992.
DOI : 10.1016/0747-7171(92)90002-L

C. Lynch and D. Tran, Automatic Decidability and Combinability Revisited, Proc. of CADE'07, 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

E. Nicolini, Combined decision procedures for constraint satisfiability, 2007.

E. Nicolini, C. Ringeissen, and M. Rusinowitch, Combinable Extensions of Abelian Groups, Proc. of CADE'09, 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, Satisfiability Procedures for Combination of Theories Sharing Integer Offsets, Proc. of TACAS'09, pp.428-442, 2009.
DOI : 10.1145/2422.322411
URL : https://hal.archives-ouvertes.fr/inria-00331735

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
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.6344

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, 2008.

I. Centre-de-recherche, ?. Nancy, and L. Est, Technopôle de Nancy-Brabois -Campus scientifique 615, rue du Jardin Botanique -BP 101 -54602 Villers-lès