Du 9 novembre au 20 décembre 2015, très prochainement donc, un MOOC sur le thème de la logique informatique sera proposé sur la plateforme FUN à destination d’un public de professeurs de mathématiques, d’étudiants en licence, d’ingénieurs, et de toute personne intéressée bien sûr !
es MOOC sont à la mode depuis quelque temps et des réflexions à propos de ces nouveaux modes d’enseignement ont lieu ici ou là. Si certains moocquent, pourquoi pas vous ? D’autant que, une fois n’est pas coutume, c’est une bande-annonce plutôt rigolote 3Attention tout de même, c’est de l’humour d’informaticien ! 😉qui nous est offerte pour démarrer :-).
Présentation du cours par les auteurs 4Ceux-là même qui portent de drôles de tee-shirts… genre de tee-shirts que portent les geeks UNIX qui passent leur temps à piper en entrée d’un programme les données issues d’un autre programme…
La logique servait surtout la philosophie et la théologie jusqu’au XIXe siècle. Elle est apparue de manière brutale et cruciale au tournant du XXe 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 permettront d’introduire plusieurs interprétations des formules, et plusieurs systèmes de preuve formelle… et le entscheindungsproblem !
Vous n’y tenez plus ? Alors pour s’inscrire et pour davantage de détails, c’est par là. Ce cours, proposé par David Baelde, Hubert Comon et Étienne Lozes de l’ENS Cachan, promet d’être vraiment très intéressant ! D’autant plus qu’on murmure déjà que d’autres saisons sont en préparation…
Homme à la pipe de Paul Cézanne.
Post-scriptum
Pour se remettre dans le bain de la logique, on pourra relire Une histoire pas très sérieuse de deux très sérieuses logiquesde Guillaume Cano, et Coqito ergo sum pour un premier aperçu sur comment vérifier un petit raisonnement logique en Coq.
ÉCRIT PAR
Aurélien Alvarez
Professeur - Rédacteur en chef d'IdM - École normale supérieure de Lyon
