Etude de la formalisation du raisonnement et aux méthodes de résolution de problèmes logiques. Cette UE étudie pour l'essentiel les propriétés des connecteurs logiques entre propositions, l'accent est donc mis sur la logique des propositions. Une introduction à la logique des prédicats sans symbole de fonction est proposée en fin d'UE. Elle est composée de 15h de cours, 22,5h de TD et de 12h de TP en salle machine pour implanter les raisonnements étudiés. Le langage support est actuellement (2017) le Scheme.
L'objectif de cette UE est d'acquérir les bases de la formalisation logique des raisonnements que ce soit dans un objectif de rédaction de preuves mathématiques ou de mise en place de systèmes de raisonnement automatique. D'un point de vue modélisation, l'objectif est d'être capable de formaliser un problème de raisonnement dans le formalisme logique et à l'inverse de "comprendre" une formule logique pour laquelle une interprétation intuitive des symboles non logiques est donnée. D'un point de vue preuve, l'objectif est d'être capable de rédiger des preuves (directe, par l'absurde, par induction...). D'un point de vue raisonnement automatique, l'objectif est de se familiariser avec les différentes techniques de résolution des problèmes logiques et d'être capable de les implanter dans un langage informatique.
- Enseignant: Daude Sylvain