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

M. Baaz and R. Iemhoff, Abstract, The Journal of Symbolic Logic, vol.121, issue.03, pp.969-998, 2008.
DOI : 10.1007/978-3-642-85983-0_11

L. Bachmair and N. Dershowitz, Completion for rewriting modulo a congruence, Proceedings 2nd Conference on Rewriting Techniques and Applications, pp.192-203, 1987.

J. Barwise, Handbook of Mathematical Logic. 4th printing edn, 1985.

R. Bonichon and O. Hermant, On Constructive Cut Admissibility in Deduction Modulo, LNCS, vol.4502, pp.33-47, 2006.
DOI : 10.1007/978-3-540-74464-1_3
URL : https://hal.archives-ouvertes.fr/hal-01337639

G. Burel, A First-Order Representation of Pure Type Systems Using Superdeduction, 2008 23rd Annual IEEE Symposium on Logic in Computer Science, pp.253-263, 2008.
DOI : 10.1109/LICS.2008.22
URL : https://hal.archives-ouvertes.fr/inria-00198543

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

G. Dowek, What Is a Theory?, 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, 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 A. Miquel, Cut elimination for Zermelo's set theory. Available on authors, p.page, 2006.

G. Dowek and B. Werner, Arithmetic as a Theory Modulo, ): RTA. LNCS, 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

J. Y. Girard, Y. Lafont, and P. Taylor, Proofs and Types, Cambridge Tracts in Theoretical Computer Science, vol.7, 1989.

O. Hermant, Semantic Cut Elimination in the Intuitionistic Sequent Calculus, pp.221-233, 2005.
DOI : 10.1007/11417170_17

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

S. C. Kleene, Mathematical Logic, 1967.

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

S. Maehara, Eine Darstellung der Intuitionistischen Logik in der Klassischen, Nagoya Mathematical Journal, vol.2, pp.45-64, 1954.
DOI : 10.1007/BF01201353

G. Mints, The Skolem method in intuitionistic calculi, Proc. Steklov Inst, pp.73-109, 1974.

G. Mints, A Short Introduction to Intuitionistic Logic. The University series in mathematics, 2000.

T. Raths, J. Otten, and C. Kreitz, The ILTP Problem Library for Intuitionistic Logic, Journal of Automated Reasoning, vol.2, issue.2, pp.261-271, 2007.
DOI : 10.1007/s10817-006-9060-z

J. Von-plato, The axioms of constructive geometry, Annals of Pure and Applied Logic, vol.76, issue.2, pp.169-200, 1995.
DOI : 10.1016/0168-0072(95)00005-2

A. Waaler and L. Wallen, Tableaux for Intutionistic Logics In: Handbook of Tableau Methods, 1999.