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.

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.

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.

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.