Outils pour le raisonnement propositionnel

Ce cours permettra de présenter les éléments de base de la logique propositionnelle et de les implanter en OCaml.

Au programme :

• Syntaxe et sémantique des formules logiques
• Tables de vérité
• Syllogismes classiques
• Déduction naturelle
• Isomorphisme Curry-Howard
• Résolution par réfutation
• Tiers exclus

Par l’étude des différents algorithmes de logique propositionnelle et de leur implantation OCaml, l’objectif de ce cours est d’amener les étudiants à comprendre comment construire un raisonnement déductif mathématique ou logique en percevant la distinction entre axiomes et propositions valides, tout en préparant l’introduction de quantificateurs qui sera vue en L3 dans la matière « Outils pour le calcul des prédicats ».

Connaitre des notions mathématiques de base : ensembles, fonctions, preuves par récurrence.

Connaissance de base en programmation fonctionnelle (OCaml).

Contrôle continu

Comprendre ce qu’est un raisonnement logique déductif

Déterminer la validité d’un raisonnement déductif

Étudier la satisfaisabilité d’une proposition

Construire un projet structuré en programmation fonctionnelle