M. Aiguier, C. Boin, and D. Longuet, On generalized theorems for normalization of proofs, 2005.

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

H. Barendregt and E. Barendsen, Autarkic computations in formal proofs, Journal of Automated Reasoning, vol.28, issue.3, pp.321-336, 2002.
DOI : 10.1023/A:1015761529444

M. P. Bonacina and N. Dershowitz, Abstract canonical inference, ACM Transactions on Computational Logic, vol.8, issue.1, 2007.
DOI : 10.1145/1182613.1182619
URL : http://arxiv.org/abs/cs/0406030

R. Bonichon, TaMeD: A Tableau Method for Deduction Modulo, Lecture Notes in Computer Science, vol.3097, pp.445-459, 2004.
DOI : 10.1007/978-3-540-25984-8_33

G. Burel and C. Kirchner, Completion Is an Instance of Abstract Canonical System Inference, Lecture Notes in Computer Science, vol.4060, pp.497-520, 2006.
DOI : 10.1007/11780274_26
URL : https://hal.archives-ouvertes.fr/inria-00000775

G. Burel and C. Kirchner, Cut elimination in deduction modulo by abstract completion (full version) Research report, 2007.

M. Crabbé, Non-normalisation de la théorie de Zermelo, 1974.

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

N. Dershowitz and C. Kirchner, Abstract saturation-based inference, 18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings., pp.65-74, 2003.
DOI : 10.1109/LICS.2003.1210046
URL : https://hal.archives-ouvertes.fr/inria-00099466

N. Dershowitz and C. Kirchner, Abstract canonical presentations, Theoretical Computer Science, vol.357, issue.1-3, pp.53-69, 2006.
DOI : 10.1016/j.tcs.2006.03.012
URL : https://hal.archives-ouvertes.fr/inria-00121760

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
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.29.2708

G. Dowek, T. Hardin, and C. Kirchner, HOL-?? an intentional first-order expression of higher-order logic, Mathematical Structures in Computer Science, vol.11, pp.1-25, 2001.
URL : https://hal.archives-ouvertes.fr/inria-00098847

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 B. Werner, Abstract, The Journal of Symbolic Logic, vol.87, issue.04, pp.1289-1316, 2003.
DOI : 10.1007/BFb0037116

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 Revised On-Line Version, Computer Science and Technology Series, vol.5, 1986.

G. Gentzen, Untersuchungen ???ber das logische Schlie???en. I, Mathematische Zeitschrift, vol.39, issue.1, pp.176-210, 1934.
DOI : 10.1007/BF01201353

O. Hermant, Méthodes Sémantiques en Déduction Modulo, 2005.

O. Hermant, Semantic Cut Elimination in the Intuitionistic Sequent Calculus, Lecture Notes in Computer Science, vol.3461, pp.221-233, 2005.
DOI : 10.1007/11417170_17

D. E. Knuth and P. B. Bendix, Simple word problems in universal algebras Computational Problems in Abstract Algebra, pp.263-297, 1970.

G. 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