France Université Numerique

Introduction à la logique informatique - Partie 1 : calcul propositionnel - ENS Cachan - Université Paris Saclay

France Université Numerique
En Ligne

Gratuit
Ou préférez-vous appeler directement le centre?

Infos importantes

Typologie Formation
Méthodologie En ligne
Début Dates au choix
  • Formation
  • En ligne
  • Début:
    Dates au choix
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!

Installations (1)
Où et quand

Lieu

Début

En ligne

Début

Dates au choixInscription ouverte

À tenir en compte

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

Questions / Réponses

Pose une question et d'autres utilisateurs vous répondrons

Qui voulez-vous pour répondre à votre question ?

On publiera seulement ton nom et prénom et ta question

Opinions

5.0
Évaluation de la formation
100%
Recommandé
4.3
fantastique
Évaluation du Centre

Opinions sur cette formation

B
BELHY STEPHANE DADIE DOBE
5.0 16/10/2018
Le meilleur de la formation: RAS
À améliorer: RAS
Recommanderiez-vous cette formation ?: Oui
* Opinions recueillies par Emagister et iAgora

Performances de ce centre

Ce centre a démontré ses qualités sur Emagister
3 ans avec Emagister

Qu'apprend-on avec cette formation ?

Calcul
Logique
Correction
Complétude de LJ
Forme clausale

Programme

Plan du cours

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

Comparer pour mieux choisir:
En voir plus