Introduction à la logique informatique - Partie 1 : calcul propositionnel
date_range Débute le 9 novembre 2015
event_note Se termine le 20 décembre 2015
list 6 séquences
assignment Niveau : Introductif
chat_bubble_outline Langue : Français
card_giftcard 7.2 points
- /5
Avis de la communauté
0 avis

Les infos clés

credit_card Formation gratuite
verified_user Certification gratuite
timer 12 heures de cours

En résumé

Ce MOOC 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!

more_horiz Lire plus
more_horiz Lire moins
dns

Le programme

Semaine 1: calcul propositionnel classique

  1. introduction du cours
  2. syntaxe
  3. sémantique
  4. satifaisabilité
  5. Entscheidungsproblem

Semaine 2: compacité et forme clausale

  1. théorème de compacité
  2. forme clausale

Semaine 3: résolution

  1. un système de preuve: la résolution
  2. correction
  3. complétude réfutationnelle
  4. complétude

Semaine 4: logique intuitionniste

  1. sémantique: structures de Kripke
  2. un système de preuve: le calcul des séquents LJ

Semaine 5: correction et complétude de LJ

  1. correction
  2. complétude

Semaine 6: perspectives

  1. calcul des séquents classique
  2. correspondance preuve-programme
  3. conclusion: quelques autres développements possibles
record_voice_over

Les intervenants

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.

store

Le concepteur

L'École normale supérieure de Cachan (aussi appelée ENS Cachan ou Normale Sup' Cachan, autrefois École normale supérieure de l'enseignement technique (ENSET), est une grande école française, faisant partie du réseau des Écoles normales supérieures.

L'ENS Cachan est un des acteurs majeurs à l'origine du cluster technologique Paris-Saclay, futur plus grand campus pluridisciplinaire d'Europe. Le déménagement de ses bâtiments sur le plateau de Saclay est prévu pour 2018.

assistant

La plateforme

France Université Numérique est le diffuseur des cours en ligne des établissements d’enseignement supérieur français et de leurs partenaires.

Il opère plusieurs plateformes de diffusion, dont la plus connue, FUN MOOC, est la première plateforme académique francophone mondiale. Grâce à de nombreux établissements partenaires, cette plateforme propose un vaste catalogue de cours s’enrichissant de jour en jour avec des thématiques variées et d’actualité.
 

Vous êtes le concepteur de ce MOOC ?
Quelle note donnez-vous à cette ressource ?
Contenu
0/5
Plateforme
0/5
Animation
0/5