Key Information
About the content
La logique servait surtout la philosophie et la théologie jusqu'au 19ème siècle. Elle est apparue de manière brutale et cruciale au tournant du 20ème siècle en mathématiques, avec les paradoxes et la question des fondements. Après le théorème de Gödel et la faillite du programme de Hilbert, la logique mathématique est devenue une partie spécialisée des mathématiques pures. Mais l'âge d'or de la logique arrive ensuite avec le développement de l'informatique.
L'utilisation des ordinateurs a forcé à formaliser complètement les problèmes à résoudre; la logique joue un rôle central dans les problèmes de spécification et de vérification des programmes. Du fait d'un lien surprenant entre les preuves et les programmes, la logique est aussi la base de la compréhension des calculs. Plus concrètement, la logique a été à l'origine d'avancées technologiques comme les langages de requêtes dans les bases de données. Beaucoup d'autres liens fondamentaux peuvent être évoqués: avec les circuits, avec la complexité, avec les jeux, avec la linguistique, etc. La logique est omniprésente en informatique.
Le cours présentera les bases de la logique informatique: cette première partie traitera de calcul propositionnel; une seconde partie, à venir, abordera la logique du premier ordre. Un perroquet menteur et des problèmes de pavage nous permettrons d'introduire plusieurs interprétations des formules, et plusieurs systèmes de preuve formelle... et le entscheindungsproblem!
Prerequisite
Ce cours s'adresse à un public large désireux de découvrir la logique informatique: professeurs de mathématiques, étudiants en licence, ingénieurs, etc. Ce cours sera un pré-requis pour les saisons à venir de ce MOOC.
Ce cours ne suppose aucune connaissance spécifique préalable, mais s'adresse cependant à un public ayant une pratique du raisonnement mathématique. Il est souhaitable d'avoir le niveau L2 en mathématiques. Il n'y a aucun pré-requis en informatique.
Conditions d’utilisation du cours :
Licence Creative Common BY-NC-ND (Attribution, Pas d’Utilisation Commerciale, Pas de Modification).
Conditions d'utilisation des contenus produits par les participants :
Licence restrictive.
Syllabus
Ce cours comportera à terme trois parties. Cette première partie, traitera de calcul propositionnel. La seconde partie portera sur la logique du premier ordre, et la troisième sur les théories axiomatiques.
Semaine 1: calcul propositionnel classique
- introduction du cours
- syntaxe
- sémantique
- satifaisabilité
- Entscheidungsproblem
Semaine 2: compacité et forme clausale
- théorème de compacité
- forme clausale
Semaine 3: résolution
- un système de preuve: la résolution
- correction
- complétude réfutationnelle
- complétude
Semaine 4: logique intuitionniste
- sémantique: structures de Kripke
- un système de preuve: le calcul des séquents LJ
Semaine 5: correction et complétude de LJ
- correction
- complétude
Semaine 6: perspectives
- calcul des séquents classique
- correspondance preuve-programme
- conclusion: quelques autres développements possibles
Instructors
David Baelde
Maître de conférences à l'ENS Cachan et chercheur en preuve formelle et sécurité des protocoles
au Laboratoire Spécification et Vérification.
Hubert Comon
Professeur à l'ENS Cachan et chercheur en logique et sécurité des protocoles
au Laboratoire Spécification et Vérification.
Etienne Lozes
Maître de conférences à l'ENS Cachan et chercheur en logique des
programmes et parallélisme au Laboratoire Spécification et Vérification.
Content Designer
The Université Paris-Saclay (French: Université Paris-Saclay) is a French federal research university which is currently under development. The project is part of the research-intensive and business cluster Paris-Saclay, located near Paris in the Plateau de Saclay. The University of Paris-Saclay is expected to be the training and research center of the Paris-Saclay technology cluster, such as Stanford University in Silicon Valley and the Technion in Israel.
Platform
France Université Numérique is the broadcaster of the online courses of French higher education institutions and their partners.
It operates several platforms of diffusion, of which the best known, FUN MOOC, is the first French-speaking academic platform worldwide. Thanks to many partner institutions, this platform offers a vast catalog of courses enriched daily with various themes and current events.
