Cette unité d'enseignement a pour objectif de raisonner sur les formalismes logiques au cœur des mathématiques et de l'informatique. Des systèmes formels de déduction sont étudiés, tant pour aider à mieux prouver manuellement des théorèmes que pour comprendre comment automatiser les preuves.
