To support our site, Class Central may be compensated by some course providers.

Introduction à la logique informatique - Partie 1 : calcul propositionnel

Université Paris-Saclay via France Université Numerique

students interested

Taken this course? Share your experience with other students. Write review

Overview

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!

Syllabus

Semaine 1: calcul propositionnel classique

introduction du cours
syntaxe
sémantique
satifaisabilité
Entscheidungsproblem

Semaine 2: compacité et forme clausale

théorème de compacité
forme clausale

Semaine 3: résolution

un système de preuve: la résolution
correction
complétude réfutationnelle
complétude

Semaine 4: logique intuitionniste

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

Semaine 5: correction et complétude de LJ

correction
complétude

Semaine 6: perspectives

calcul des séquents classique
correspondance preuve-programme
conclusion: quelques autres développements possibles

Taught by

Hubert Comon

Review for France Université Numerique's Introduction à la logique informatique - Partie 1 : calcul propositionnel
5.0 Based on 1 reviews

  • 5 star 100%
  • 4 star 0%
  • 3 star 0%
  • 2 star 0%
  • 1 star 0%

Did you take this course? Share your experience with other students.

Write a review
  • 1
Longton L
5.0 a year ago
by Longton completed this course.
Was this review helpful to you? Yes
  • 1

Class Central

Get personalized course recommendations, track subjects and courses with reminders, and more.

Sign up for free

Never stop learning Never Stop Learning!

Get personalized course recommendations, track subjects and courses with reminders, and more.