P. B. Andrews, Resolution in type theory, The Journal of Symbolic Logic, pp.414-432, 1971.

L. Bachmair and H. Ganzinger, Resolution Theorem Proving, Handbook of Automated Reasoning, 2001.
DOI : 10.1016/B978-044450813-3/50004-7

G. Burel, Embedding Deduction Modulo into a Prover, 2010.
DOI : 10.1007/978-3-642-15205-4_15

G. Burel and G. Dowek, How can we prove that a proof search method is not an instance of another? Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, ACM International Conference Proceeding Series, 2009.

G. Dowek, What Is a Theory?, Symposium on Theoretical Aspects of Computer Science, pp.50-64, 2002.
DOI : 10.1007/3-540-45841-7_3

G. Dowek, Simple Type Theory as a clausal theory, 2010.

G. Dowek, . Th, C. Hardin, and . Kirchner, HOL-lambda-sigma: an intentional firstorder expression of higher-order logic, Mathematical Structures in Computer Science, vol.11, pp.1-25, 2001.
URL : https://hal.archives-ouvertes.fr/hal-01199524

G. Dowek, . Th, C. Hardin, and . 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

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

G. Huet, A mechanisation of Type Theory, Third International Joint Conference on Artificial Intelligence, pp.139-146, 1973.

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

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

J. R. Slagle, Automatic Theorem Proving With Renamable and Semantic Resolution, Journal of the ACM, vol.14, issue.4, pp.687-697, 1967.
DOI : 10.1145/321420.321428

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