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

D. Beauqier, J. Berstel, and C. Philippe, Éléments d'algorithmique, 1992.

C. Lee, Symbolic Logic and Mechanical Theorem Proving, Computer Science and Applied Mathematics, 1973.

H. Thomas, C. E. Cormen, R. L. Leiserson, C. Rivest, and . Stein, Introduction to Algorithms, p.3, 2009.

R. David, K. Nour, and C. Raffalli, Introduction à la logique, 2003.
URL : https://hal.archives-ouvertes.fr/hal-00396917

H. Ebbinghaus, Jörg Flum et Wolfgang Thomas, 1994.

, Undergraduate Texts in Mathematics

M. Fitting, First-Order Logic and Automated Theorem Proving. Graduate Texts in Computer Science, 1996.
DOI : 10.1007/978-1-4612-2360-3

J. Goubault-larrecq and I. Mackie, Proof Theory and Automated Deduction, Applied Logic Series, vol.6, p.de, 1997.
DOI : 10.1007/978-94-011-3981-6

G. Huet, Résolution d'équations dans les langages d'ordre 1, 2, 1976.

R. Lassaigne and . Michel-de-rougemont, Logic and Complexity. Discrete Mathematics and Theoretical Computer Science, 2004.

S. Michael, . Paterson, N. Mark, and . Wegman, Linear unification, Journal of Computer and System Sciences, vol.16, issue.2, pp.158-167, 1978.

R. E. Tarjan and J. Van-leeuwen, Worst-case analysis of set union algorithms, Journal of the ACM, vol.31, issue.2, pp.245-281, 1984.
DOI : 10.1145/62.2160

URL : http://www.csd.uwo.ca/~eschost/Teaching/07-08/CS445a/p245-tarjan.pdf