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

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, 2008.
DOI : 10.1145/1459010.1459014

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

L. Bachmair, A. Tiwari, and L. Vigneron, Abstract Congruence Closure, Journal of Automated Reasoning, vol.31, issue.2, pp.129-168, 2003.
DOI : 10.1023/B:JARS.0000009518.26415.49

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

C. W. Barrett, D. L. Dill, and A. Stump, A generalization of Shostak's method for combining decision procedures, Proc. of the 4th International Workshop on Frontiers of Combining Systems, FroCoS'02, pp.132-147, 2002.

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

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

A. Boudet, Combining Unification Algorithms, Journal of Symbolic Computation, vol.16, issue.6, pp.597-626, 1993.
DOI : 10.1006/jsco.1993.1066

URL : http://doi.org/10.1006/jsco.1993.1066

M. Bozzano, R. Bruttomesso, A. Cimatti, T. Junttila, S. Peter-van-rossum 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

URL : http://doi.org/10.1016/j.ic.2005.05.011

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 (VMCAI'06), pp.427-442, 2006.
DOI : 10.1007/11609773_28

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

S. Conchon and S. Krsti´ckrsti´c, Strategies for combining decision procedures Conference on Tools and Algorithms for the Construction and Analysis of Systems, Proc. of the 9th Int, pp.537-553, 2003.

S. Conchon and S. Krsti´ckrsti´c, Canonization for disjoint unions of theories, Proc. of the 19th International Conference on Automated Deduction (CADE'03), pp.197-211, 2003.

D. Cyrluk, P. Lincoln, and N. Shankar, On Shostak's decision procedure for combinations of theories, Proc. of the 13th International Conference on Automated Deduction, pp.463-477, 1996.
DOI : 10.1007/3-540-61511-3_107

L. De-moura, H. Rueß, and N. Shankar, Justifying Equality, Selected Papers from the Workshops on Disproving and the Second International Workshop on Pragmatics of Decision Procedures Issue 3 of Electronic Notes in Theoretical Computer Science (ENTCS), pp.69-85, 2004.
DOI : 10.1016/j.entcs.2004.06.068

N. Dershowitz and J. Jouannaud, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, chapter 6: Rewrite Systems, pp.244-320, 1990.

D. Detlefs, G. Nelson, and J. B. Saxe, Simplify: a theorem prover for program checking, Journal of the ACM, vol.52, issue.3, pp.365-473, 2005.
DOI : 10.1145/1066100.1066102

P. J. Downey, R. Sethi, and R. E. Tarjan, Variations on the Common Subexpression Problem, Journal of the ACM, vol.27, issue.4, pp.758-771, 1980.
DOI : 10.1145/322217.322228

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

P. Fontaine, Techniques for Verification of Concurrent Systems with Invariants, 2004.

P. Fontaine, J. Marion, S. Merz, L. P. Nieto, and A. Tiu, Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants, 12th Intl
DOI : 10.1007/3-540-45620-1_26

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

. Conf, Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol.3920, pp.167-181, 2006.

H. Ganzinger, Shostak Light, Proc. of the 18th International Conference on Automated Deduction, pp.332-346, 2002.
DOI : 10.1007/3-540-45620-1_28

S. Ghilardi, E. Nicolini, S. Ranise, and D. Zucchelli, Decision procedures for extensions of the theory of arrays, Annals of Mathematics and Artificial Intelligence, vol.27, issue.1, pp.3-4231, 2007.
DOI : 10.1007/s10472-007-9078-x

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

D. Kapur, Shostak's congruence closure as completion, Proc. of Rewriting Techniques and Applications, 8th International ConferenceRTA'97), pp.23-37, 1997.
DOI : 10.1007/3-540-62950-5_59

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

D. Kapur, A Rewrite Rule Based Framework for Combining Decision Procedures *, Proc. of the 4th Int. Workshop on Frontiers of Combining Systems, pp.87-102, 2002.
DOI : 10.1007/3-540-45988-X_8

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

H. Kirchner, S. Ranise, C. Ringeissen, and D. Tran, Automatic Combinability of Rewriting-Based Satisfiability Procedures, Proc. of the 13th Int. Conference on Logic for Programming, pp.542-556, 2006.
DOI : 10.1007/11916277_37

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

Z. Manna and C. G. Zarba, Combining decision procedures In Formal Methods at the Cross Roads: From Panacea to Foundational Support, LNCS, vol.2757, pp.381-422, 2003.

C. Marché, Normalized Rewriting: an Alternative to Rewriting modulo a Set of Equations, Journal of Symbolic Computation, vol.21, issue.3, pp.253-288, 1996.
DOI : 10.1006/jsco.1996.0011

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

R. Nieuwenhuis and A. Oliveras, Proof-Producing Congruence Closure, Proc. of the 16th International Conference on Rewriting Techniques and ApplicationsRTA'05), pp.453-468, 2005.
DOI : 10.1007/978-3-540-32033-3_33

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

R. Nieuwenhuis and A. Rubio, Paramodulation-Based Theorem Proving, Hand. of Automated Reasoning, 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

T. Nipkow, Combining matching algorithms: The regular case, Journal of Symbolic Computation, vol.12, issue.6, pp.633-653, 1991.
DOI : 10.1016/S0747-7171(08)80145-9

S. Ranise, C. Ringeissen, and D. Tran, Nelson-Oppen, Shostak and the Extended Canonizer: A Family Picture with a Newborn, Proc. of First International Colloquium on Theoretical Aspects of Computing, pp.372-386, 2004.
DOI : 10.1007/978-3-540-31862-0_27

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

S. Ranise, C. Ringeissen, and D. Tran, Combining Proof-Producing Decision Procedures, Proc. of the 6th Int. Symposium on Frontiers of Combining Systems, pp.237-251, 2007.
DOI : 10.1007/978-3-540-74621-8_16

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

H. Rueß and N. Shankar, Deconstructing Shostak, Proceedings 16th Annual IEEE Symposium on Logic in Computer Science, pp.19-28, 2001.
DOI : 10.1109/LICS.2001.932479

H. Rueß and N. Shankar, Combining shostak theories, Proc. of the 13th International Conference on Rewriting Techniques and Applications, pp.1-18, 2002.

R. Sebastiani, Lazy Satisfiability Modulo Theories, Journal on Satisfiability , Boolean Modeling and Computation (JSAT), vol.3, pp.141-224, 2007.

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

A. Stump and L. Tang, The Algebra of Equality Proofs, Proc. of the 16th International Conference on Rewriting Techniques and Applications (RTA), pp.469-483, 2005.
DOI : 10.1007/978-3-540-32033-3_34

R. E. Tarjan, Efficiency of a Good But Not Linear Set Union Algorithm, Journal of the ACM, vol.22, issue.2, pp.215-225, 1975.
DOI : 10.1145/321879.321884

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

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