L. Bachmair, N. Dershowitz, and D. Plaisted, Completion without failure Resolution of Equations in Algebraic Structures Rewriting Techniques, pp.1-30, 1989.

L. Bachmair and H. Ganzinger, Rewrite-based Equational Theorem Proving with Selection and Simplification, Journal of Logic and Computation, vol.4, issue.3, pp.1-31, 1994.
DOI : 10.1093/logcom/4.3.217

L. Bachmair and H. Ganzinger, Resolution Theorem Proving, pp.19-99, 2001.
DOI : 10.1016/B978-044450813-3/50004-7
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.113.4450

G. Burel, From axioms to rewriting rules, available on author's web page

G. Burel, Experimenting with Deduction Modulo, LNCS, vol.43, issue.4, pp.162-176, 2011.
DOI : 10.1007/978-3-642-02959-2_10
URL : https://hal.archives-ouvertes.fr/hal-01125858

D. Cousineau and G. Dowek, Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo, pp.102-117, 2007.
DOI : 10.1007/978-3-540-73228-0_9

A. Degtyarev and A. Voronkov, Equality Reasoning in Sequent-Based Calculi, pp.611-706, 2001.
DOI : 10.1016/B978-044450813-3/50012-6

D. Delahaye, D. Doligez, F. Gilbert, P. Halmagrand, and O. Hermant, Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo, LNCS, vol.8312, pp.274-290, 2013.
DOI : 10.1007/978-3-642-45221-5_20
URL : https://hal.archives-ouvertes.fr/hal-00909784

N. Dershowitz, M. Okada, and G. Sivakumar, Confluence of conditional rewrite systems, Proceedings 1st International Workshop on Conditional Term Rewriting Systems, pp.31-44, 1987.
DOI : 10.1007/3-540-19242-5_3

G. Dowek, What Is a Theory?, LNCS, vol.2285, pp.50-64, 2002.
DOI : 10.1007/3-540-45841-7_3

G. Dowek, Confluence as a Cut Elimination Property, ) RTA. LNCS, pp.2-13, 2003.
DOI : 10.1007/3-540-44881-0_2

G. Dowek, Polarized Resolution Modulo, TCS. IFIP AICT, vol.323, pp.182-196, 2010.
DOI : 10.1007/978-3-642-15240-5_14
URL : https://hal.archives-ouvertes.fr/hal-01054460

G. Dowek, T. Hardin, and C. Kirchner, Theorem proving modulo, Journal of Automated Reasoning, vol.31, issue.1, pp.33-72, 2003.
DOI : 10.1023/A:1027357912519
URL : https://hal.archives-ouvertes.fr/hal-01199506

H. Ganzinger and J. Stuber, Superposition with equivalence reasoning and delayed clause normal form transformation, Information and Computation, vol.199, issue.1-2, pp.3-23, 2005.
DOI : 10.1016/j.ic.2004.10.010
URL : https://hal.archives-ouvertes.fr/inria-00099710

O. Hermant, Resolution is Cut-Free, Journal of Automated Reasoning, vol.15, issue.2, pp.245-276, 2009.
DOI : 10.1007/s10817-009-9153-6
URL : https://hal.archives-ouvertes.fr/hal-00743218

J. Hurd, M. Bobaru, K. Havelund, G. J. Holzmann, and R. Joshi, The OpenTheory Standard Theory Library, NFM 2011, pp.177-191, 2011.
DOI : 10.1007/3-540-60275-5_76

M. Jacquel, K. Berkani, D. Delahaye, and C. Dubois, Tableaux modulo theories using superdeduction ? an application to the verification of B proof rules with the Zenon automated theorem prover, LNCS, vol.7364, pp.332-338, 2012.
URL : https://hal.archives-ouvertes.fr/hal-01126134

D. E. Knuth and P. B. Bendix, Simple Word Problems in Universal Algebras, Computational Problems in Abstract Algebra, pp.263-297, 1970.
DOI : 10.1007/978-3-642-81955-1_23

J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM, vol.12, issue.1, pp.23-41, 1965.
DOI : 10.1145/321250.321253

S. G. Vorobyov, On the arithmetic inexpressiveness of term rewriting systems, [1988] Proceedings. Third Annual Information Symposium on Logic in Computer Science, pp.212-217, 1988.
DOI : 10.1109/LICS.1988.5120