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

S. Berezin, V. Ganesh, and D. L. Dill, An Online Proof-Producing Decision Procedure for Mixed-Integer Linear Arithmetic, Proceedings of TACAS'03, 2003.
DOI : 10.1007/3-540-36577-X_38

N. S. Bjørner, Integrating Decision Procedures for Temporal Verification, 1998.

L. De-moura, H. Rueß, and N. Shankar, Justifying Equality, PDPAR, 2004.
DOI : 10.1016/j.entcs.2004.06.068

D. Déharbe and S. Ranise, Light-weight theorem proving for debugging and verifying units of code, First International Conference onSoftware Engineering and Formal Methods, 2003.Proceedings., 2003.
DOI : 10.1109/SEFM.2003.1236224

J. Filliâtre, S. Owre, H. Rueß, and N. Shankar, ICS: Integrated Canonizer and Solver?, Computer Aided Verification (CAV), volume 2102 of LNCS, pp.246-249, 2001.
DOI : 10.1007/3-540-44585-4_22

P. Fontaine and P. Gribomont, Combining Non-stably Infinite, Non-first Order Theories, Pragmatics of Decision Procedures in Automated Reasoning, 2004.
DOI : 10.1016/j.entcs.2004.06.066

H. Ganzinger and . Shostak-light, Automated Deduction ? CADE-18, LNCS, vol.2392, pp.332-346, 2002.

D. Kapur and X. Nie, Reasoning about Numbers in Tecton, Proc. 8 th Inl. Symp. Methodologies for Intelligent Systems, pp.57-70, 1994.

T. F. Melham, Automating Recursive Type Definitions in Higher Order Logic, Current Trends in Hardware Verification and Theorem Proving, pp.341-386, 1989.
DOI : 10.1007/978-1-4612-3658-0_9

G. Nelson and D. C. Oppen, Fast Decision Procedures Based on Congruence Closure, Journal of the ACM, vol.27, issue.2, pp.356-364, 1980.
DOI : 10.1145/322186.322198

D. C. Oppen, Reasoning About Recursively Defined Data Structures, Journal of the ACM, vol.27, issue.3, pp.403-411, 1980.
DOI : 10.1145/322203.322204

S. Owre and N. Shankar, Abstract Datatypes in PVS, 1997.

L. C. Paulson, A fixedpoint approach to implementing (Co)inductive definitions, Automated Deduction ? CADE-12, LNAI 814, pp.148-161
DOI : 10.1007/3-540-58156-1_11

W. Pugh, The omega test: a fast integer programming algorithm for dependence analysis. Supercomputing, pp.4-13, 1991.

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, C. W. Barrett, and D. L. Dill, CVC: A Cooperating Validity Checker, Computer Aided Verification (CAV), pp.500-504, 2002.
DOI : 10.1007/3-540-45657-0_40

C. Tinelli and C. G. Zarba, Combining Non-Stably Infinite Theories, Electronic Notes in Theoretical Computer Science, vol.86, issue.1, 2004.
DOI : 10.1016/S1571-0661(04)80651-0

P. Wolper and B. Boigelot, On the Construction of Automata from Linear Arithmetic Constraints, TACAS, pp.1-19, 2000.
DOI : 10.1007/3-540-46419-0_1

C. G. Zarba, Combining Multisets with Integers, Automated Deduction ? CADE-18, pp.363-376, 2002.
DOI : 10.1007/3-540-45620-1_30

C. G. Zarba, Combining Sets with Integers, Frontiers of Combining Systems, pp.103-116, 2002.
DOI : 10.1007/3-540-45988-X_9

C. G. Zarba, Combining Sets with Elements, Theory and Practice, pp.762-782, 2004.
DOI : 10.1007/978-3-540-39910-0_33

T. Zhang, H. B. Sipma, and Z. Manna, Decision Procedures for Recursive Data Structures with Integer Constraints, Automated Reasoning, pp.152-167, 2004.
DOI : 10.1007/978-3-540-25984-8_9