v2.11.0 (5648)

Programme d'approfondissement - CSC_51051_EP : Logique Informatique : de l'Intelligence Artificielle à l'Absence d'erreurs

Domaine > Informatique.

Illustration de la fiche

Descriptif

La logique informatique est utilisé dans un large éventail d'applications en informatique, allant de l'approche déductive de l'Intelligence Artificielle préconisée par le pionnier de l'IA, John McCarthy, à la démonstration de l'absence de bogues dans de grands logiciels industriels, comme la ligne 14 du métro de Paris, ou à vérifier les théorèmes difficiles comme celui de Feit-Thompson dans la classification des groupes simples finis.

L'objectif de ce cours est d'expliquer la manière dont la logique peut être utilisée afin de modéliser des problèmes de nature informatique ou mathématique, et comment les ordinateurs peuvent être utilisés pour y parvenir. Nous allons présenter des assistants de preuve, qui permettent de formaliser un raisonnement humain par la construction interactive de preuves, et expliquent leur utilité pour certifier l'absence de bogues dans les programmes. Il est basé sur la correspondance Curry-Howard : un programme est identique à une preuve (ou plus précisemment, un programme fonctionnel typé correspond à une dérivation de son type). Afin d'atteindre des applications réalistes, nous présenterons l'assistant de preuve Agda et la logique dépendente qu'il sous tend. Si le temps nous le permet, nous présenterons également différentes notions et techniques telles que la théorie des ensembles et la recherche de preuve.

Ce cours est aussi à propos de logique en pratique : toutes les PC se feront sur ordinateurs, utilisant OCaml puis Agda.

 

Site du cours : http://inf551.mimram.fr/

Objectifs pédagogiques

Les notions suivantes seront progressivement introduites :

  • logique propositionnelle et les variations constructives,
  • programmation fonctionnelle, formalisée par lambda-calcul,
  • systèmes de typage et la correspondance Curry-Howard.

Pour les étudiants du diplôme Programmes d'échange internationaux

Aucun

Pour les étudiants du diplôme M2 CPS - Système Cyber Physique

Aucun

Pour les étudiants du diplôme M1 CPS - Système Cyber Physique

Aucun

Pour les étudiants du diplôme Titre d’Ingénieur diplômé de l’École polytechnique

INF412 conseillé (mais pas obligatoire)

Pour les étudiants du diplôme M1 MPRI - Fondements de l'Informatique

Aucun

Format des notes

Numérique sur 20

Littérale/grade réduit

Pour les étudiants du diplôme M1 CPS - Système Cyber Physique

Vos modalités d'acquisition :

La note finale est le résultat de la moyenne des trois composantes suivantes :

  • la moyenne de la note des TDs (TD4 excepté)
  • le TD4 qui fait office de projet
  • l'examen final

L'UE est acquise si Note finale >= 10
  • Crédits ECTS acquis : 5 ECTS

Pour les étudiants du diplôme M2 CPS - Système Cyber Physique

Vos modalités d'acquisition :

La note finale est le résultat de la moyenne des trois composantes suivantes :

  • la moyenne de la note des TDs (TD4 excepté)
  • le TD4 qui fait office de projet
  • l'examen final

Le rattrapage est autorisé (Note de rattrapage conservée)
    L'UE est acquise si Note finale >= 10
    • Crédits ECTS acquis : 5 ECTS

    Pour les étudiants du diplôme Titre d’Ingénieur diplômé de l’École polytechnique

    Vos modalités d'acquisition :

    La note finale est le résultat de la moyenne des trois composantes suivantes :

    • la moyenne de la note des TDs (TD4 excepté)
    • le TD4 qui fait office de projet
    • l'examen final

    Le rattrapage est autorisé (Note de rattrapage conservée)
      L'UE est acquise si note finale transposée >= C
      • Crédits ECTS acquis : 5 ECTS

      La note obtenue rentre dans le calcul de votre GPA.

      Pour les étudiants du diplôme M1 MPRI - Fondements de l'Informatique

      Vos modalités d'acquisition :

      La note finale est le résultat de la moyenne des trois composantes suivantes :

      • la moyenne de la note des TDs (TD4 excepté)
      • le TD4 qui fait office de projet
      • l'examen final

      Le rattrapage est autorisé (Note de rattrapage conservée)
        L'UE est acquise si Note finale >= 10
        • Crédits ECTS acquis : 5 ECTS

        Pour les étudiants du diplôme Programmes d'échange internationaux

        Vos modalités d'acquisition :

        La note finale est le résultat de la moyenne des trois composantes suivantes :

        • la moyenne de la note des TDs (TD4 excepté)
        • le TD4 qui fait office de projet
        • l'examen final

        Le rattrapage est autorisé (Note de rattrapage conservée)
          L'UE est acquise si note finale transposée >= C
          • Crédits ECTS acquis : 5 ECTS

          La note obtenue rentre dans le calcul de votre GPA.

          Veuillez patienter