Introduction à la logique informatique - Partie 1 : calcul propositionnel

Introduction à la logique informatique - Partie 1 : calcul propositionnel

Archived
课程
fr
法语
12 时
此内容评级为 5/5

你无法访问存档的 讲座

来源
  • 来自www.fun-mooc.fr
状况
  • 免费获取
  • 免费证书
更多信息
  • 6 序列
  • 等级 介绍
  • 从11 十一月 2015开始
  • 以18 十一月 2015结束

你无法访问存档的 讲座

他们的员工每天都在学习Edflex

  • Safran
  • Air France
  • TotalEnergies
  • Generali
Learn more

课程详情

教学大纲

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

先决条件

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.

讲师

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.

编辑

巴黎-萨克雷大学(University of Paris-Saclay)于2019年成立,旨在以法国前所未有的水平发展从基础科学到应用科学的知识体系,强调跨学科性和面向世界的开放性。它是 1971 年 1 月 1 日成立的巴黎第十一大学(Universidad de Paris-Sud-XI)的继承者,其目标是通过国际最高水平的研究,促进对社会面临的重大问题的认识。巴黎-萨克雷大学为学生提供前瞻性的教育框架和内容。实验室与社会经济参与者之间的持续互动使前沿研究成果得以转化为创新成果。

十九所创始院校为巴黎-萨克雷大学带来了各自闻名遐迩的优势:教育与研究之间的紧密联系、国际标准的实验室和主要研究设施、在工程和管理培训方面的国际声誉以及种类繁多的高水平课程。

除合作伙伴提供的资源外,该计划还得到了巴黎-萨克雷 IDEX 的资助,将支持为该校学生开设 MOOC 和 SPOC 课程,以及面向社会经济界的继续教育课程(与社会经济界已有密切联系)。

平台

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

此内容评级为 5/5
(没有评论)
此内容评级为 5/5
(没有评论)
完成这个资源,写一篇评论