J. and 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

A. Robinson and A. , Voronkov: Handbook of Automated Reasioning, 2001.

G. Burel, Experimenting with Deduction Modulo, 2011.
DOI : 10.1007/978-3-642-02959-2_10
URL : https://hal.archives-ouvertes.fr/hal-01125858

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

G. Dowek, Polarized Resolution Modulo, IFIP Theoretical Computer Science, 2010.
DOI : 10.1007/978-3-642-15240-5_14
URL : https://hal.archives-ouvertes.fr/hal-01054460

G. Dowek, Proofs and Algorithms: An Introduction to Logic and Computability, 2011.
DOI : 10.1007/978-0-85729-121-9

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