1  Programme

1.1  Planning

Le cours comporte 14 séances. Les 7 premières séances se déroulent au premier semestre le mardi de 9h à 12h en salle C321 et sont assurées par Christine Paulin.

• 22 septembre
  • cours : calcul propositionnel, syntaxe, sémantique
  • développement : lemme de compacité
• 29 septembre
  • cours : calcul propositionnel, diagrammes de décision binaires, systèmes de preuve (Hilbert, Déduction naturelle, Calcul des Séquents)
  • développements : canonicité de la représentation des obdd, complétude du calcul des séquents
• 6 octobre
  • cours : calcul propositionnel, résolution
  • développements : exemple de preuve en calcul des séquents de taille exponentielle, complétude de la résolution binaire
• Jeudi 15 octobre
  • cours : calcul des prédicats
• 20 octobre
  • cours : calcul des prédicats
• 3 novembre
  • cours : calcul des prédicats
• 10 novembre
  • cours : calcul des prédicats

1.2  Leçons concernées

• 916-Formules du calcul propositionnel : représentation, formes normales, satisfiabilité. Applications.
• 917-Logique du premier ordre : syntaxe et sémantique.
• 918-Systèmes formels de preuve en logique du premier ordre : exemples
• 924-Théories et modèles en logique du premier ordre. Exemples
• 919-Unification : algorithmes et applications
• 920-Réécriture et formes normales. Exemples

1.3  Notes de cours

• Logique propositionnelle
  • Notes pour la préparation à l’agrégation
  • Cours de Jean Goubault Logique propositionnelle, P, NP
• Cours de Hubert Comon Logique
• Calcul des prédicats
  • Notes pour la préparation à l’agrégation

Références

[1]

Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.

[2]

Olivier Carton. Langages Formels Calculabilité et Complexité. Vuibert, 2008.

[3]

Robert Cori and Daniel Lascar. Logique Mathématique. Axiomes. Masson, 1993.

[4]

René David, Karim Nour, and Christophe Raffalli. Introduction à la Logique. Théorie de la démonstration (2ème édition). Sciences Sup. Dunod, 2004.

[5]

Stéphane Devismes, Pascal Lafourcade, and Michel Lévy. Informatique théorique : Logique et démonstration automati que, Introduction à la logique propositionnelle et à la logique du premier o rdre. Ellipses, 2012.

[6]

Jean H. Gallier. Logic for Computer Science, Fooundations of Automatic Theorem Proving. Wiley, 1987.

[7]

Jean Goubault-Larrecq and Ian Mackie. Proof Theory and Automated Deduction, volume 6 of Applied Logic Series. Kluwer Academic Publishers, May 1997.

[8]

René Lalement. Logique, réduction, résolution. Masson, 1990.

[9]

Hans Zantema. Total termination of term rewriting is undecidable. J. Symb. Comput., 20(1):43–60, 1995.

2  Liens utiles

• Informations sur l’agrégation de mathématique
• Leçons 2014 de l’option informatique
• Emploi du temps

Ce document a été traduit de L^AT_EX par H^EV^EA