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

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

E. Tushkanova, A. Giorgetti, C. Ringeissen, and O. Kouchnarenko, A Rule-Based Framework for Building Superposition-Based Decision Procedures, Proc. of 9th Int. Workshop on Rewriting Logic and Its Applications (WRLA'2012), pp.2012-221
DOI : 10.1007/978-3-642-34005-5_12
URL : https://hal.archives-ouvertes.fr/hal-00749576

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-51, 2009.
DOI : 10.1145/1459010.1459014
URL : https://hal.archives-ouvertes.fr/inria-00576862

N. Dershowitz and J. Jouannaud, Rewrite Systems, Volume B: Formal Models and Sematics (B), pp.243-320, 1990.
DOI : 10.1016/B978-0-444-88074-1.50011-1

A. Armando, M. Bonacina, S. Ranise, and S. Schulz, On a Rewriting Approach to Satisfiability Procedures: Extension, Combination of Theories and an Experimental Appraisal, Proc. of the 5th Int. Workshop on Frontiers of Combining Systems (FroCoS'2005), pp.65-80, 2005.
DOI : 10.1007/11559306_4

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

E. Nicolini, C. Ringeissen, and M. Rusinowitch, Combinable Extensions of Abelian Groups, Proc. of 22nd International Conference on Automated Deduction (CADE'2009), 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 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'2009), pp.428-442, 2009.
DOI : 10.1145/2422.322411
URL : https://hal.archives-ouvertes.fr/inria-00331735

E. Tushkanova, C. Ringeissen, A. Giorgetti, and O. Kouchnarenko, Automatic Decidability for Theories with Counting Operators, RTA'13, pp.303-318, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00920496

. Audacy, Automated decidability and combinability -web interface, 2014.

M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-oliet et al., The Maude 2.0 System, Proc. of 14th Int. Conference on Rewriting Techniques and Applications (RTA'2003), pp.76-87, 2003.
DOI : 10.1007/3-540-44881-0_7

M. Clavel, F. Durán, S. Eker, S. Escobar, P. Lincoln et al., Unification and Narrowing in Maude 2.4, Proc. of 20th Int. Conference on Rewriting Techniques and Applications (RTA'2009), pp.380-390, 2009.
DOI : 10.1007/3-540-45446-2_27

N. Martí-oliet, J. Meseguer, and A. Verdejo, Towards a Strategy Language for Maude, Electronic Notes in Theoretical Computer Science, vol.117, pp.417-441, 2005.
DOI : 10.1016/j.entcs.2004.06.020

S. Eker, N. Martí-oliet, J. Meseguer, and A. Verdejo, Deduction, Strategies, and Rewriting, Electronic Notes in Theoretical Computer Science, vol.174, issue.11, pp.3-25, 2007.
DOI : 10.1016/j.entcs.2006.03.017
URL : http://doi.org/10.1016/j.entcs.2006.03.017

E. Tushkanova, Schematic calculi for the analysis of decision procedures, 2013.
URL : https://hal.archives-ouvertes.fr/tel-01037993

C. Ringeissen and V. Senni, Modular Termination and Combinability for Superposition Modulo Counter Arithmetic, Proc. of 8th International Symposium on Frontiers of Combining Systems (FroCoS'2011), pp.211-226, 2011.
DOI : 10.1007/978-3-642-04222-5_20
URL : https://hal.archives-ouvertes.fr/inria-00636589

F. Durán and J. Meseguer, A Church-Rosser Checker Tool for Conditional Order-Sorted Equational Maude Specifications, Proc. of 8th Int. Workshop on Rewriting Logic and Its Applications (WRLA'10), pp.69-85, 2010.
DOI : 10.1007/978-3-642-16310-4_6

F. Durán and J. Meseguer, A Maude Coherence Checker Tool for Conditional Order-Sorted Rewrite Theories, Proc. of 8th Int. Workshop on Rewriting Logic and Its Applications (WRLA'10), pp.86-103, 2010.
DOI : 10.1007/978-3-642-16310-4_7

J. C. Blanchette and A. Paskevich, TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism, 24th International Conference on Automated Deduction, Lake Placid, pp.414-420, 2013.
DOI : 10.1007/978-3-642-38574-2_29
URL : https://hal.archives-ouvertes.fr/hal-00825086

S. Krstic, A. Goel, J. Grundy, and C. Tinelli, Combined Satisfiability Modulo Parametric Theories, 13th International Conference, pp.602-617, 2007.
DOI : 10.1007/978-3-540-71209-1_47