
Pourquoi formaliser ? Cartographie du raisonnement.
Logique propositionnelle : syntaxe et sémantique.
Systèmes de déduction.
Correction, complétude et décidabilité de la logique propositionnelle.
Premier ordre : langage, termes et structures.
Conséquence et preuve au premier ordre.
Complétude de Gödel.
Compacité et usages.
Löwenheim–Skolem et pluralité des modèles.
Théories axiomatiques, Zermelo-Fraenkel et axiome du choix.
Syntaxe arithmétisée et diagonalisation.
Incomplétude de Gödel et ouverture sur le calcul.
- Titulaire: Mickaël RANDOUR

Logique et fondements des systèmes intelligents
Logique, langage et calcul.
Langages et automates.
Machines de Turing et fonctions calculables.
Décidabilité.
Complexité.
Logiques décidables.
SAT et SMT.
Lambda-calcul et types.
Lean en pratique.
Une introduction aux LLMs.
Ouverture sur les méthodes formelles.
- Titulaire: Mickaël RANDOUR

Comprendre les objets mathématiques nécessaires aux sciences de la vie, maîtriser les concepts fondamentaux des outils mathématiques classiques, savoir les mettre en pratique dans des cas concrets, développer la rigueur nécessaire au raisonnement formel.
- Titulaire: Mickaël RANDOUR
- Assistant: Chloé CAPON
- Assistant: Quentin LAMBOTTE

Comprendre en profondeur les concepts fondateurs des méthodes formelles, maîtriser leurs fondements mathématiques, savoir les mettre en pratique dans des cas concrets à l'aide d'outils logiciels, pouvoir intégrer les méthodes formelles dans un processus de développement logiciel, être capable d'aborder des travaux avancés dans le domaine.
- Enseignant: Mickaël RANDOUR
- Assistant: Sougata BOSE
- Assistant: Chloé CAPON