La logique est la formalisation du raisonnement humain. À ce titre, elle
est au carrefour de diverses activités, qu'elles soient scientifiques ou non.

En mathématiques, il est courant de démontrer des théorèmes, mais
comment se convaincre que la preuve que l'on énonce est correcte, ne souffre
pas de raccourcis un peu rapides ?

En informatique, il est courant d'écrire des programmes, mais comment
se convaincre que l'algorithme puis le code que l'on a produits sont
corrects ?

Dans la vie de tous les jours, il est courant d'argumenter des points de
vue ou d'écouter ceux d'autrui, mais comment se convaincre que ces
arguments ne sont pas fallacieux, comment être certain que l'on
enchaîne nos arguments de manière irréprochable pour convaincre nos
auditeurs ?

Savoir ce qu'est une preuve dans un formalisme logique revient donc à
comprendre quelles sont les déductions valides dans ce formalisme. Savoir ce
qu'est une preuve est un atout d'auto-défense intellectuelle aidant à
se prémunir contre l'approximatif et la tromperie, ce qui est à mon avis
important pour tout scientifique (si ce n'est pour tout citoyen).

Ce cours a plusieurs objectifs:

• aborder la logique en tant que science, comme objet d'étude et
  démontrer des propriétés sur certains formalismes logiques
• aborder la logique en tant qu'outil, pour formaliser des problèmes et
  démontrer des propriétés
• aborder la logique en tant qu'outil, pour formaliser des programmes et
  démontrer des propriétés
• aborder la logique comme domaine sur lequel des algorithmes peuvent
  travailler pour automatiser des vérifications de preuves, voire (en
  partie) des recherches de preuves

Il ne sera pas question d'étudier tous les formalismes logiques tant ils
sont nombreux et rapidement complexes. On commencera par étudier le calcul
propositionnel qui permet de formaliser assez simplement la notion de
correction d'une démonstration. Ensuite on s'intéressera au calcul des
prédicats qui permet de formuler une plus grande classe de propriétés.
On examinera quelques formalismes pour ces deux fragments de la logique
(principalement un système à la Frege-Hilbert, la déduction naturelle et
le calcul des séquent).

Le cours mélangera des aspects purement théoriques (démonstrations au sens
« habituel » du terme), des aspects programmation en OCaml pour travailler
sur des formules logiques, des aspects preuve et programmation en Coq
pour mettre en application les « preuves formelles ».

Enfin, nous verrons le lien entre preuves et programmes (correspondance
de Curry-Howard en faisant un détour par la calculabilité et le
lambda-calcul. À ce sujet, on se restreindra sans doute restreinte à la
logique minimale pour ne pas devoir aborder des lambda-calculs compliqués.

Sur la forme, le cours se déroulera sous forme de « cours/TD intégrés »,
alternant les activités « cours » et « application ». Il s'étendra sur
8 séances (dont un contrôle des connaissances).

M1 E3A - UE444 - Programmation systèmes et réseaux