next up previous contents index
suivant: Index monter: Logique et démonstration automatique précédent: 6. Déduction naturelle au   Table des matières   Index

Bibliographie

1
Collin Allen and Michael Hand.
Logic Primer.
MIT, 2001.

2
Peter B. Andrews.
An introduction to mathematical logic : to truth through proof.
Academic Press, 1986.

3
Franz Baader and Wayne Snyder.
Unification theory.
In John Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning (in 2 volumes), pages 445-532. Elsevier and MIT Press, 2001.

4
Alonzo Church.
A note on the entscheidungsproblem.
Journal of Symbolic Logic, 1(1):40-41, 1936.

5
Stephen A. Cook.
The complexity of theorem-proving procedures.
In Proceedings of the third annual ACM symposium on Theory of computing, STOC '71, pages 151-158, New York, NY, USA, 1971. ACM.

6
René Cori and Daniel Lascar.
Logique mathématique Cours et exercices I. Calcul propositionnel, algèbres de Boole, calcul des prédicats.
Masson, 1993.

7
René Cori and Daniel Lascar.
Logique mathématique Cours et exercices II. Fonctions récursives, théorème de Gödel, théorie des ensembles, théories des modèles.
Masson, 1993.

8
René David, Karim Nour, and Christophe Raffali.
Introduction à la logique.
Dunod, 2001.

9
Martin Davis, George W. Logemann, and Donald W. Loveland.
A machine program for theorem-proving.
Communications of The ACM, 5:394-397, 1962.

10
Martin Davis and Hilary Putnam.
A computing procedure for quantification theory.
Journal of the ACM (JACM), 7(3):201-215, 1960.

11
Herbert B. Enderton.
A mathematical Introduction to Logic.
Academic Press, 2001.

12
Gerhard Gentzen.
Untersuchungen über das logische Schließen I.
Mathematische Zeitschrift, 39:176-210, 1935.
10.1007/BF01201353.

13
Gerhard Gentzen.
Untersuchungen über das logische Schließen II.
Mathematische Zeitschrift, 39:405-431, 1935.
10.1007/BF01201363.

14
Roger Godement.
Cours d'algèbre.
Hermann, 1973.

15
Gérard P. Huet.
unification in typed lambda calculus.
In Corrado Böhm, editor, Lambda-Calculus and Computer Science Theory, Proceedings of the Symposium Held in Rome, March 25-27, 1975, volume 37 of Lecture Notes in Computer Science, pages 192-212. Springer, 1975.

16
Gérard P. Huet.
Higher order unification 30 years later.
In Victor Carreño, César Muñoz, and Sofiène Tahar, editors, Theorem Proving in Higher Order Logics, 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002, Proceedings, volume 2410 of Lecture Notes in Computer Science, pages 3-12. Springer, 2002.

17
Michael Huth and Mark Ryan.
Logic in Computer Science.
Cambridge University Press, 2004.

18
Jacquemin.
Logique et Mathématiques 109 exercices corrigées.
Masson, 1994.

19
Stephen C. Kleene.
Logique Mathématique.
Armand Colin, 1971.

20
Thierry Lucas, Isabelle Berlanger, and Isabelle De Greef.
Initiation à la logique formelle.
De Boeck, 2003.

21
Alberto Martelli and Ugo Montanari.
An efficient unification algorithm.
ACM Trans. Program. Lang. Syst., 4:258-282, April 1982.

22
William McCune.
Prover9 and mace4.
http://www.cs.unm.edu/~mccune/prover9/, 2005-2010.

23
J. Alan Robinson.
A machine-oriented logic based on the resolution principle.
Journal of the ACM (JACM), 12(1):23-41, January 1965.

24
Alan Turing.
On computable numbers, with an application to the entscheidungsproblem.
Proceedings of the London Mathematical Society, 42:230-265, 1937.



Benjamin Wack 2013-01-08