Introduction à la logique informatique - Partie 2 : calcul des prédicats
- Durée : 6 semaines
- Effort : 12 heures
- Rythme: ~2 heures/semaine
- Langues: NA
Description
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.
Après la première partie traitait de calcul propositionnel, cette seconde partie aborde la logique du premier ordre.
Aussi appelé calcul des prédicats, c'est le langage dans lequel on exprime la plupart des mathématiques, mais aussi un grand nombre d'applications de la logique en informatique. Retrouvez l'équipe enseignante, ses puzzles favoris et le fameux entscheindungsproblem, pour découvrir la richesse de ce langage!
Format
Ce cours se déroule sur six semaines. Chaque semaine, nous vous proposons:
- environ quarante-cinq minutes de vidéos, découpées en deux à quatre segments ;
- des quizz ;
- des notes de cours, incluant des exercices d'approfondissement.
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.
Il est fortement recommandé d'avoir suivi la première partie du cours de logique informatique avant de suivre cette deuxième partie.
Dans son ensemble, 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.
Evaluation et Certification
Ce cours contient des quiz hebdomadaires
Plan de cours
- 1. introduction du cours
2. syntaxe
3. F-algèbres
- 1. (F-P)-structures
2. axiomes de l'égalité
3. exemples de satisfaction - 1. (F-P)-structures
2. axiomes de l'égalité
3. exemples de satisfaction
- 1. forme prénexe
2. skolémisation
3. forme clausale
4. théorème de Herbrand
- 1. unification
2. résolution
- 1. calcul des séquent LK1
2. correction
3. recherche de preuve
4. complétude
- 1. clauses de Horn
2. programmation logique
3. conclusion: ouvertures
Équipe pédagogique
DAVID BAELDE
Catégories
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
Catégories
Professeur à l'ENS Cachan et chercheur en logique et sécurité des protocoles au Laboratoire Spécification et Vérification.
ETIENNE LOZES
Catégories
Maître de conférences à l'ENS Cachan et chercheur en logique des programmes et parallélisme au Laboratoire Spécification et Vérification.