Partager cette page :
Discipline(s) : Infomatique et télécommunications

Fondements de l'informatique 2 : logique

Semestre Semestre 2
Type Obligatoire
Nature UE
Crédits ECTS 6
Volume horaire total 40
Volume horaire CM 20
Volume horaire TD 20

Responsables

Pré-requis

Bases de la logique propositionnelle. Preuves par récurrence.

Objectifs

À la fin du cours, les étudiants ont acquis une bonne intuition des différences et des connexions entre syntaxe et sémantique, entre preuve et calcul.
Ils ont renforcé leurs capacités de rigueur dans le raisonnement, et commencé à discerner ce qui est calculable de ce qui ne l'est pas dans le domaine de la vérification.

Contenu

Description

L'objectif de ce cours est de fournir les bases de logique indispensables pour la poursuite d'études en informatique. Le cours montre comment la logique propositionnelle et la logique du 1er ordre permettent de formaliser le raisonnement. Il s'attache en particulier à manipuler différents systèmes de déduction et à comparer leurs avantages respectifs dans une perspective de mécanisation.


Programme

A – Calcul propositionnel 
1. Syntaxe et sémantique du calcul propositionnel
2. Systèmes de déduction : déduction intuitionniste et classique, calcul des séquents, preuves par coupure
 
B – Logique du 1er ordre
1. Syntaxe d’une logique du 1er ordre
2. Sémantique d’une logique du 1er ordre, notion de modèle
3. Systèmes de déduction pour la logique du 1er ordre : déduction naturelle, séquents, résolution, unification et programmation logique
4. Validité et complétude d’un système de déduction
5. Exemples de théories. Théories décidables et récursives. Axiomatisation. Théorèmes d’incomplétude.
 
C –  Pour aller plus loin (au choix)
1. Logiques temporelles
2. Raisonnement équationnel et réécriture

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.

Contrôles des connaissances

Durant le semestre, contrôle continu (CC) sous forme de devoir et projet.
En session de rattrapage, un examen oral (O).
Note finale en session 1 : CC
Note finale en session 2 : O

Mise à jour le 12 juillet 2017