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

F. Baader and K. U. Schulz, Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures, Journal of Symbolic Computation, vol.21, issue.2, pp.211-243, 1996.
DOI : 10.1006/jsco.1996.0009

M. P. Bonacina and M. Echenim, T-decision by decomposition, Proc. of CADE'07, pp.199-214, 2007.

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 IJCAR'06, pp.513-527, 2006.
DOI : 10.1007/11814771_42

A. Boudet, J. Jouannaud, and M. Schmidt-schauß, Unification in Boolean Rings and Abelian Groups, Journal of Symbolic Computation, vol.8, issue.5, pp.267-296, 1990.
DOI : 10.1016/S0747-7171(89)80054-9

P. L. Chenadec, Canonical Forms in Finitely Presented Algebras. Research Notes in Theoretical Computer Science, 1986.

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

N. Dershowitz, Orderings for term-rewriting systems, Theoretical Computer Science, vol.17, issue.3, pp.279-301, 1982.
DOI : 10.1016/0304-3975(82)90026-3

P. C. Eklof and G. Sabbagh, Model-completions and modules, Annals of Mathematical Logic, vol.2, issue.3, pp.251-295, 1971.
DOI : 10.1016/0003-4843(71)90016-7

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

G. Godoy and R. Nieuwenhuis, Superposition with completely built-in Abelian groups, Journal of Symbolic Computation, vol.37, issue.1, pp.1-33, 2004.
DOI : 10.1016/S0747-7171(03)00070-1

M. J. Hall, The Theory of Groups, 1968.

W. Hodges, Model Theory. Number 42 in Encyclopedia of Mathematics and its Applications, 1993.

K. Korovin and A. Voronkov, Integrating Linear Arithmetic into Superposition Calculus, Proc. of CSL'07, pp.223-237
DOI : 10.1007/978-3-540-74915-8_19

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

G. E. Peterson and M. E. Stickel, Complete Sets of Reductions for Some Equational Theories, Journal of the ACM, vol.28, issue.2, pp.233-264, 1981.
DOI : 10.1145/322248.322251

G. Plotkin, Building-in equational theories, Machine Intelligence, vol.7, pp.73-90, 1972.

J. Stuber, Superposition theorem proving for abelian groups represented as integer modules, Theoretical Computer Science, vol.208, issue.1-2, pp.149-177, 1998.
DOI : 10.1016/S0304-3975(98)00082-6

U. Waldmann, Superposition and Chaining for Totally Ordered Divisible Abelian Groups, Proc. of IJCAR'01, pp.226-241, 2001.
DOI : 10.1007/3-540-45744-5_17

U. Waldmann, Cancellative Abelian Monoids and Related Structures in Refutational Theorem Proving (Part II), Journal of Symbolic Computation, vol.33, issue.6, pp.777-829, 2002.
DOI : 10.1006/jsco.2002.0537

T. Zhang, Arithmetic integration of decision procedures 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, 2006.