L’objectif de cette UE est d’aborder la démonstration et la recherche de preuves automatique suivant deux axes: un premier qui consiste à proposer des méthodes de déduction et recherche de preuves en logique des prédicats du premier ordre et un second qui consiste à étudier la mécanisation de la preuve de programmes avec une mise en œuvre avec un assistant de preuve.
Prérequis
Aucun.
Acquis d’apprentissage
- Méthodes de preuves
- logique des prédicats du 1er ordre
- méthodes des tableaux : calcul propositionnel et calcul des prédicats
- méthodes des connexions : calcul propositionnel et calcul des prédicats
- Preuves de programmes
- présentation d’une preuve formelle à la main
- logique propositionnelle en Coq
- quantificateurs et types inductifs simples
- prédicats inductifs et preuves par induction
- étude et complétion d’une version mécanisée de d’une preuve formelle
Compétences visées
- Maîtriser des méthodes de preuve et leur automatisation.
- Vérifier des propriétés de programmes à l’aide d’un assistant de preuve.