Niveau d'étude
BAC +3
ECTS
4,5 crédits
Composante
UFR Sciences et Techniques
Description
Ce cours permettra d’approfondir les éléments présentés dans la matière « outils pour la logique propositionnelle » (L2 informatique) et les étendre au calcul des prédicats (ajout des quantificateurs), tout en conservant un lien fort avec la pratique de la programmation fonctionnelle par l’implantation OCaml des algorithmes présentés.
Au programme :
- Rappels de logique propositionnelle
- Algorithme de Quine
- Déduction classique
- Syntaxe et sémantique du calcul des prédicats
- Déduction naturelle et prédicats
- Isomorphisme Curry-Howard
- Skolemisation et résolution
Objectifs
Par l’étude des différents algorithmes du calcul des prédicats et de leur implantation OCaml, l’objectif de ce cours est d’amener les étudiants à comprendre comment construire un raisonnement déductif mathématique ou logique à l’aide de quantificateurs classiques, tout en mettant en œuvre des techniques avancées de programmation fonctionnelle par l’intermédiaire de l’isomorphisme Curry-Howard.
Pré-requis obligatoires
Connaitre des notions mathématiques de base : ensembles, fonctions, preuves par récurrence.
Connaissance de base en programmation fonctionnelle (OCaml).
Connaitre les notions suivantes de logique propositionnelle : formule, évaluation, tables de vérité, déduction naturelle, résolution par réfutation.
Contrôle des connaissances
Contrôle continu 60%
TP 40%
Compétences visées
Comprendre ce qu’est un raisonnement logique
Déterminer la validité d’un raisonnement déductif
Étudier la satisfaisabilité d’une proposition quantifiée
Construire un projet structuré en programmation fonctionnelle