Introduction à la logique informatique - Partie 1 : calcul propositionnel
date_range 开始2015年11月12日
event_note 结束于2015年11月19日
list 6个序列
assignment 等级:入门
chat_bubble_outline 语言 : 法语
card_giftcard 96点
评论
-
starstarstarstarstar

关键信息

credit_card 免费进入
verified_user 免费证书
timer 总共12个小时

关于内容

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!

more_horiz 查看更多
more_horiz 收起
report_problem

前提

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 sera un pré-requis pour les saisons à venir de ce MOOC.

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.

Conditions d’utilisation du cours :
Licence Creative Common BY-NC-ND (Attribution, Pas d’Utilisation Commerciale, Pas de Modification).

Conditions d'utilisation des contenus produits par les participants :
Licence restrictive.

dns

课程大纲

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

  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

教师

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

内容设计师

Université Paris-Saclay

L’Université Paris-Saclay a été conçue pour développer à un niveau inédit en France le continuum des connaissances depuis les sciences fondamentales jusqu’aux sciences appliquées, mettant l’accent sur l’interdisciplinarité et l’ouverture sur le monde. Son objectif est de faire avancer la connaissance sur les grands enjeux de société grâce à une recherche au plus haut niveau international. L’Université Paris-Saclay offre ainsi aux étudiants un cadre et un contenu de formation tournés vers l’avenir. Les interactions permanentes entre laboratoires et acteurs socio-économiques permettent de transformer des résultats d’une recherche de pointe en innovations.

Les dix-neuf institutions fondatrices apportent à l’Université Paris-Saclay les forces qui font leur réputation : lien étroit entre formation et recherche, laboratoires et grands instruments de recherche aux standards internationaux, réputation internationale des formations d’ingénieurs et de managers, cursus diversifiés de haut niveau.

Pour soutenir l’offre de formations communes portées par l’Université Paris-Saclay, et donner les moyens aux partenaires d’enrichir leur propre offre de formation, l’Université Paris-Saclay a conçu le programme « former avec le numérique » qui s’inscrit dans la dynamique de création du Learning center de l’Université.

Ce programme, doté par l’IDEX Paris-Saclay en appui des moyens mis par les partenaires, accompagne la création de MOOC et celle de SPOC pour les étudiants de l’Université, ainsi que pour des usages de formation continue vers le monde socio-économique avec lequel les contacts sont déjà forts.

assistant

平台

FUN

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

你是这个MOOC的设计者?
您对这门课的评价是 ?
内容
0/5
平台
0/5
动画
0/5