Logique, Preuve de programme, Induction

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.

Session 1 ou session unique - Contrôle des connaissances

Session 2 - Contrôle des connaissances