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, pp.1-451, 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

Y. Boichut, T. Genet, T. P. Jensen, and L. L. Roux, Rewriting Approximations for Fast Prototyping of Static Analyzers, Lecture Notes in Computer Science, vol.4533, pp.48-62, 2007.
DOI : 10.1007/978-3-540-73449-9_6
URL : https://hal.archives-ouvertes.fr/hal-00463418

Y. Boichut, P. Héam, and O. Kouchnarenko, Handling Algebraic Properties in Automatic Analysis of Security Protocols, Lecture Notes in Computer Science, vol.4281, pp.153-167, 2006.
DOI : 10.1007/11921240_11
URL : https://hal.archives-ouvertes.fr/hal-00463424

M. Clavel, F. Durán, S. Eker, S. Escobar, P. Lincoln et al., Unification and Narrowing in Maude 2.4, Rewriting Techniques and E
DOI : 10.1007/3-540-45446-2_27

M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-oliet et al., The Maude 2.0 System, Int. Conf. RTA 2003, pp.76-87, 2003.
DOI : 10.1007/3-540-44881-0_7

N. Dershowitz and J. Jouannaud, Rewrite systems Handbook of Theoretical Computer Science, Formal Models and Semantics, pp.243-320, 1990.

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

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

C. Lynch, S. Ranise, C. Ringeissen, and D. Tran, Automatic decidability and combinability, Information and Computation, vol.209, issue.7, pp.1026-1047, 2011.
DOI : 10.1016/j.ic.2011.03.005
URL : https://hal.archives-ouvertes.fr/inria-00586936

E. Nicolini, C. Ringeissen, and M. Rusinowitch, Combinable Extensions of Abelian Groups, Int. Conf. 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, LNCS, vol.31, issue.2, 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, 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

E. Tushkanova, A. Giorgetti, C. Ringeissen, and O. Kouchnarenko, A Rule-Based Framework for Building Superposition-Based Decision Procedures, Inria RESEARCH CENTRE NANCY ? GRAND EST 615 rue du Jardin Botanique CS20101 54603 Villers-lès-Nancy Cedex Publisher Inria Domaine de Voluceau -Rocquencourt BP 105 -78153 Le Chesnay Cedex inria.fr ISSN, pp.164-182, 2012.
DOI : 10.1007/978-3-642-34005-5_12
URL : https://hal.archives-ouvertes.fr/hal-00749576