F. Baader and T. Nipkow, Term Rewriting and all That, 1998.

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, Handbook of Automated Reasoning, pp.19-99, 2001.
DOI : 10.1016/B978-044450813-3/50004-7

R. Bonichon and O. Hermant, A Semantic Completeness Proof for TaMeD, Lecture Notes in Computer Science, vol.4246, pp.167-181, 2006.
DOI : 10.1007/11916277_12
URL : https://hal.archives-ouvertes.fr/hal-01337086

G. Burel, Automating Theories in Intuitionistic Logic, FroCoS. Lecture Notes in Artificial Intelligence, vol.76, pp.181-197, 2009.
DOI : 10.1016/0168-0072(95)00005-2
URL : https://hal.archives-ouvertes.fr/inria-00395934

G. Burel, Embedding Deduction Modulo into a Prover, Lecture Notes in Computer Science, vol.6247, pp.155-169, 2010.
DOI : 10.1007/978-3-642-15205-4_15

G. Burel, Experimenting with Deduction Modulo, Lecture Notes in Artificial Intelligence, 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

G. Burel and G. Dowek, How can we prove that a proof search method is not an instance of another?, Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages Theory and Practice, LFMTP '09, pp.84-87, 2009.
DOI : 10.1145/1577824.1577838

G. Burel and C. Kirchner, Regaining cut admissibility in deduction modulo using abstract completion, Information and Computation, vol.208, issue.2, pp.140-164, 2010.
DOI : 10.1016/j.ic.2009.10.005
URL : https://hal.archives-ouvertes.fr/inria-00132964

A. Ciabattoni, N. Galatos, and K. Terui, From Axioms to Analytic Rules in Nonclassical Logics, 2008 23rd Annual IEEE Symposium on Logic in Computer Science, 2008.
DOI : 10.1109/LICS.2008.39

G. Dowek, What Is a Theory?, STACS. Lecture Notes in Computer Science, vol.2285, pp.50-64, 2002.
DOI : 10.1007/3-540-45841-7_3

G. Dowek, Confluence as a Cut Elimination Property, Lecture Notes in Computer Science, vol.2706, 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, HOL-?? an intentional first-order expression of higher-order logic, Mathematical Structures in Computer Science, vol.11, issue.1, pp.1-25, 2001.
URL : https://hal.archives-ouvertes.fr/hal-01199524

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

G. Dowek and A. Miquel, Cut elimination for Zermelo's set theory, 2006.

G. Dowek and B. Werner, Arithmetic as a Theory Modulo, Lecture Notes in Computer Science, vol.3467, pp.423-437, 2005.
DOI : 10.1007/978-3-540-32033-3_31

J. H. Gallier, Logic for Computer Science: Foundations of Automatic Theorem Proving, Computer Science and Technology Series, vol.5, 1986.

J. Gao, Clausal Presentation of Theories in Deduction Modulo, Journal of Computer Science and Technology, vol.208, issue.2, 2011.
DOI : 10.1007/s11390-013-1399-0
URL : https://hal.archives-ouvertes.fr/inria-00614251

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

F. Kirchner, A Finite First-Order Theory of Classes, Lecture Notes in Computer Science, vol.4502, pp.188-202, 2006.
DOI : 10.1007/978-3-540-74464-1_13

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

S. Negri and J. Von-plato, Abstract, Bulletin of Symbolic Logic, vol.4, issue.04, pp.418-435, 1998.
DOI : 10.2307/420956

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

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

L. Wos, G. A. Robinson, and D. F. Carson, Efficiency and Completeness of the Set of Support Strategy in Theorem Proving, Journal of the ACM, vol.12, issue.4, pp.536-541, 1965.
DOI : 10.1145/321296.321302