Le MOOC Introduction à la logique informatique 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!
* MOOC Francophone est un service de mise en relation sans inscription et sans intermédiaire. Nous n’organisons aucun cours, le lien « Suivre le cours » vous redirige vers la page web des organisateurs. Les participants peuvent également évaluer ce cours en cliquant ici
Intervenant
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.Durée
6 semaines
Du 16 novembre au 20 décembre 2015Prérequis
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.
Charge de travail
2 heures / semaine
Coût
Gratuit
Certification
L’attestation de suivi avec succès FUN sera uniquement basée sur les réponses aux quizz.
Déroulement
Ce cours se déroule sur six semaines. Chaque semaine, nous vous proposons:
– environ quarante-cinq minutes de vidéos, découpées en deux à quatre segments ;
– des quizz ;
– des notes de cours, incluant des exercices d’approfondissement.Programme
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 clausaleSemaine 3: résolution
– Un système de preuve: la résolution
– Correction
– Complétude réfutationnelle
– ComplétudeSemaine 4: logique intuitionniste
– Sémantique: structures de Kripke
– Un système de preuve: le calcul des séquents LJSemaine 5: correction et complétude de LJ
– Correction
– ComplétudeSemaine 6: perspectives
– Calcul des séquents classique
– Correspondance preuve-programme
– Conclusion: quelques autres développements possiblesPlateforme
France Université Numérique (FUN)
Plate-forme nationale française et propriété du Ministère de l’Enseignement Supérieur et de la Recherche. Elle est basée sur la technologie Open edX du MIT et de Harvard.
Merci pour votre contribution. Votre avis est en attente de modération avant publication. Après validation, vos données seront anonymisées.
Taux de satisfaction
Votre perception du cours doit rester constructive. Nous encourageons un débat sain et constructif entre concepteurs de MOOC et utilisateurs. Les avis sont modérés avant publication et les données sont anonymisées après contrôle. Pour évaluer ce cours, cliquez sur le lien bleu - Je participe ! - et validez votre accord avec chacune des affirmations sur une échelle de 1 à 100. Merci de votre compréhension !
