17250007 - Logique

Licence 3 - Semestre 6 - MAJEURE Philosophie - UE Fondamentale - Année universitaire 2025-26

Enseignante : Faustine OLIVA

Titre du cours :  Preuves, programmes et types : de la correspondance preuves-programmes aux assistants de preuve

Programme du cours :
La logique, en tant qu'objet d'étude et qu'ensemble de méthodes et d'outils, entretient des rapports étroits avec différentes disciplines parmi lesquelles les mathématiques et l'informatique. Les travaux relatifs à la correspondance preuves-programmes illustrent une manière dont ces trois disciplines peuvent interagir. L'appellation ? correspondance preuves-programmes ? désigne un ensemble de résultats qui mettent en évidence une correspondance structurelle entre systèmes logiques et modèles de calcul : les preuves formalisées dans les premiers peuvent être vues comme des programmes informatiques tels que décrits dans les deuxièmes. Il est donc possible de mobiliser des techniques et des résultats issus de l'informatique et de la programmation pour étudier et manipuler des preuves, notamment des démonstrations mathématiques formalisées. S'appuyant sur ces découvertes les travaux autour de la mécanisation et de l'automatisation des démonstrations mathématiques et de leur vérification se sont multipliés ces dernières années. Ces développements ont mené à la conception et à l'élaboration d'un nouveau type de logiciel : les assistants de preuve. L'idée est de permettre à l'utilisateur de formaliser une démonstration plus ou moins complexe dans un langage de programmation de manière à ce que l'assistant puisse en vérifier la validité.  Suite aux succès de différents projets de formalisation et de vérification la communauté mathématique est de plus en plus encline à intégrer ces nouveaux outils à ses activités.
 
Ce champ de recherche et ses réalisations les plus récentes soulèvent des questions conceptuelles (qu'est-ce qu'une démonstration ?), épistémologiques (quelle est la nature de la connaissance mathématique associée à une démonstration assistée par ordinateur ?) et pratiques (comment l'usage des assistants de preuve impacte-t-il l'élaboration des connaissances à l'échelle d'une communauté de recherche ?).
 
Ce cours consistera à mettre à disposition des étudiants les connaissances historiques et philosophiques ainsi que les savoir-faire techniques nécessaires à la compréhension de ce qu'est la correspondance preuves-programmes et de ce que sont les assistants de preuve. Cela en vue de leur permettre de conduire une réflexion substantielle et cohérente sur les questions conceptuelles et épistémologiques évoquées ci-dessus.
 
L'objectif de ce cours est de donner aux étudiants qui se destinent à une spécialisation en philosophie des sciences, en particulier en logique, en philosophie des mathématiques et en philosophie de l'informatique, un aper?u des questionnements qui structurent un champ de recherche en pleine expansion. Aux étudiants qui se tourneront vers d'autres domaines de recherche il s'agit de proposer des exemples concrets leur permettant de nourrir leur réflexion : les questions abordées dans ce cours, quoique techniques et spécifiques, peuvent aisément être mises en relation avec des questions philosophiques plus générales telle que le rapport du sujet humain aux machines et aux nouvelles technologies. Concernant celles et ceux qui ne se retrouveraient dans aucune des deux catégories précédentes, l'auteure de ces lignes espère que, aussi décriée soit-elle, la curiosité intellectuelle continue de mouvoir les promotions de jeunes philosophes et que ce cours saura répondre à leurs attentes.
 

Terminal écrit (TE) 4h.

Crédits ECTS : 3