Fondements 2 : logique

Bibliographie

• Logique et fondements de l'informatique : logique du 1er ordre, calculabilité et lambda-calcul, R. Lassaigne, M. de Rougemont.
• Logique mathématique, cours et exercices, vol 1 & 2, R. Cori, D. Lascar.
• Fondements mathématiques de l'informatique, J. Stern.
• Logique, réduction, résolution, R. Lalement.
• Handbook of Logic in Computer Science, vol 1, S. Abramsky, D.M. Gabbay, T.S.E. Maibaum.
• Introduction à la calculabilité , P. Wolper.
• Vérification de logiciels : techniques et outils du model-checking, Ph. Schnoebelen, B. Bérard, M. Bidoit, F. Laroussinie, et A. Petit.

Contenu

1. Introduction à la logique. Généralités sur l'induction. Syntaxe et sémantique du calcul propositionnel. Formes normales.
2. Compacité du calcul propositionnel. Systèmes de déduction : preuve et réfutation par coupure (validité et complétude).
3. Systèmes de déduction pour le calcul propositionnel : déduction naturelle minimale, intuitionniste et classique, calcul des séquents classique.
4. Calcul des prédicats : syntaxe et sémantique. Notion de modèle. Équivalences sémantiques usuelles.
5. Sémantique du calcul des prédicats : formes prénexes, formes de Skolem. Préservation de l'existence d'un modèle lors de la skolémisation. Notion de théorie et de conséquence sémantique. Systèmes de déduction pour le calcul des prédicats : déduction naturelle. Cohérence des théories.
6. Validité et complétude de la déduction naturelle. Compacité du calcul des prédicats. Calcul des séquents au 1er ordre.
7. Logique constructive (G. Dowek).
8. Exemples de théories : égalité, arithmétique. Théories décidables et récursives. Axiomatisation finie. Incomplétude.
9. Méthode de résolution. Algorithme d'unification.
10. Validité et complétude de la résolution. Programmation logique.
11. Logique équationnelle et réécriture.

Examens

• Le sujet d'examen de l'année 2013-2014.