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 à comprendre la notion de preuve (manuelle) que pour évoquer l'automatisation possible des preuves.
- Syntaxe et sémantique du logique propositionnelle, formes normales
- Modélisation SAT et recherche de modèle par simplification et algorithme DPLL, utilisation de SAT-solveurs
- Calcul des séquents en logique propositionnelle : théorèmes de correction et complétude
- Syntaxe et sémantique de la logique des prédicats
- Théories logiques : théories axiomatiques, élimination des quantificateurs, théorie des ordres denses et théories arithmétiques
- Satisfiabilité modulo théorie, utilisation de SMT-solveurs
- Calcul des séquents en logique des prédicats
