La logique est la formalisation du raisonnement humain. À ce titre; elleest 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; maiscomment se convaincre que la preuve que l'on énonce est correcte; ne souffrepas de raccourcis un peu rapides ? En informatique; il est courant d'écrire des programmes; mais commentse convaincre que l'algorithme puis le code que l'on a produits sontcorrects ? Dans la vie de tous les jours; il est courant d'argumenter des points devue ou d'écouter ceux d'autrui; mais comment se convaincre que cesarguments ne sont pas fallacieux; comment être certain que l'onenchaîne nos arguments de manière irréprochable pour convaincre nosauditeurs ? Savoir ce qu'est une preuve dans un formalisme logique revient donc àcomprendre quelles sont les déductions valides dans ce formalisme. Savoir cequ'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 avisimportant 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 etdémontrer des propriétés sur certains formalismes logiques aborder la logique en tant qu'outil; pour formaliser des problèmes etdémontrer des propriétés aborder la logique en tant qu'outil; pour formaliser des programmes etdémontrer des propriétés aborder la logique comme domaine sur lequel des algorithmes peuventtravailler pour automatiser des vérifications de preuves; voire (enpartie) des recherches de preuves Il ne sera pas question d'étudier tous les formalismes logiques tant ilssont nombreux et rapidement complexes. On commencera par étudier le calculpropositionnel qui permet de formaliser assez simplement la notion decorrection d'une démonstration. Ensuite on s'intéressera au calcul despré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 etle 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 travaillersur des formules logiques; des aspects preuve et programmation en Coqpour mettre en application les « preuves formelles ». Enfin; nous verrons le lien entre preuves et programmes (correspondancede Curry-Howard en faisant un détour par la calculabilité et lelambda-calcul. À ce sujet; on se restreindra sans doute restreinte à lalogique 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 sur8 séances (dont un contrôle des connaissances).
