Composante
École Nationale Supérieure d'Électrotechnique d'Électronique d'Informatique d'Hydraulique et des Télécommunications
Objectifs
Introduire la notion de vérification de programmes par la preuve. Utiliser un assistant de preuve.
Description
– Logique des propositions et des prédicats.
– Démonstration de tautologies en utilisant la déduction naturelle et le principe de résolution.
– Induction sur les ensembles.
– Induction structurelle de Burstall.
– Application à la preuve de programme récursifs par induction.
– Présentation et utilisation d’un assistant de preuve.