FUN CAMPUS
  • Actualités
  • Cours
  • Organisations
  • A propos de FUN Campus
  • Accès enseignant
  • Mon compte
  • Nous contacter
  • Vous êtes ici:
  • Accueil
  • Cours
  • Introduction à la logique informatique - Partie 1 : calcul propositionnel
InformatiqueLicenceMathématiques

Introduction à la logique informatique - Partie 1 : calcul propositionnel

  • Durée : 6 semaines
  • Effort : 2 heures/semaine
logo d'établissement principal

Vous êtes enseignant et souhaitez utiliser ce cours avec vos étudiants ?

Nous contacter

Description

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!

Format

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.

Prérequis

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 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.

Evaluation et Certification

Ce cours comporte des quiz hebdomadaires

Plan de cours

    • 1. introduction du cours
      2. syntaxe
      3. sémantique
      4. satifaisabilité
      5. Entscheidungsproblem
    • 1. théorème de compacité
      2. forme clausale
    • 1, un système de preuve: la résolution
      2. correction
      3. complétude réfutationnelle
      4. complétude
    • 1. sémantique: structures de Kripke
      2. un système de preuve: le calcul des séquents LJ
    • 1. correction
      2. complétude
    • - calcul des séquents classique
      - correspondance preuve-programme
      - conclusion: quelques autres développements possibles

Équipe pédagogique

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.

Établissements

ENS Paris-Saclay

En savoir plus

  • Qui sommes-nous ?
  • A propos de Fun Campus
  • Mentions légales
  • Charte utilisateur
  • Politique de confidentialité
  • Conditions d'utilisation
  • Aide et contact

Des formations pour enrichir les cursus

FacebookTwitterLinkedin
Propulsé par Richie