suivant: Index
monter: Logique et démonstration automatique
précédent: 6. Déduction naturelle au
Table des matières
Index
- 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