Logique et mathématiques discrète
avec Manuel Lafond
Introduction
Manuel Lafond
Logique
Étude des mathématiques en tant que langage.
Représenter des énoncés formellement avec des
formules.
Prouver des énoncés de façon rigoureuse avec des
règles de dérivation.
Axiomes = énoncés de « départ »
Théorèmes = énoncés dérivables logiquement à
partir des axiomes
Manuel Lafond
Manuel Lafond
Mathématiques discrètes
Discret = dénombrable, que l’on peut énumérer
• ex: liste d’étudiants, instructions d’un programme, état
de la mémoire, nombres entiers
• ex non-discret: les réels entre 0 et 1
Maths discrètes = étude des structures discrètes
• Graphes et réseaux
• Automates
• Complexité algorithmique
• Théorie des l’information
• …
Manuel Lafond
Objectifs du cours
1. Représenter des énoncés en formule mathématique
ex: La somme de deux nombres entiers pairs est un
nombre pair.
Manuel Lafond
Objectifs du cours
1. Représenter des énoncés en formule mathématique
ex: La somme de deux nombres entiers pairs est un
nombre pair.
Manuel Lafond
Objectifs du cours
2. Interpréter des formules mathématiques
ex:
Manuel Lafond
Objectifs du cours
3. Évaluer une formule mathématique
• (voir si elle est vraie ou fausse, ou satisfaisable)
• Parfois à l’aide d’outils de vérification (Tarski-UdeS, Pro-B)
Manuel Lafond
Objectifs du cours
4. Prouver des énoncés.
• 4.1: En langue naturelle:
• Théorème: La somme de deux nombres entiers pairs
est un nombre pair.
• Preuve. Soit 𝑥 et 𝑦 deux nombres entiers pairs.
Puisque 𝑥 est pair, il existe un entier 𝑖 tel que 𝑥 = 2𝑖.
De la même façon, il existe un entier 𝑗 tel que 𝑦 = 2𝑗.
La somme de 𝑥 et 𝑦 est donc 𝑥 + 𝑦 = 2𝑖 + 2𝑗 =
2(𝑖 + 𝑗). Puisque 𝑥 + 𝑦 est un multiple de 2, la
somme de 𝑥 et 𝑦 est paire.
Manuel Lafond
Objectifs du cours
Prouver des énoncés.
En symboles:
Manuel Lafond
Objectifs du cours
Prouver des énoncés.
En notation par séquents:
Manuel Lafond
Buts en informatique de MAT115
développer une approche rigoureuse en
programmation
pouvoir spécifier formellement le comportement
attendu d'un programme
• Permet ensuite de vérifier le programme
Manuel Lafond
Buts en informatique de MAT115
pouvoir démontrer qu'un algo fait ce qu'il prétend
pouvoir évaluer le temps qu’un algorithme
AVANT de le coder!
Manuel Lafond
Buts en informatique de MAT115
Et bien plus …
• comprendre les mécanismes internes d'un ordinateur
(ordinateur = connecteurs logiques et, ou, xor, ...)
• comprendre les bases de données relationnelles
• comprendre les fondements de la théorie du calcul
– Machines de Turing, complexité, décidabilité
Manuel Lafond
Manuel Lafond
Manuel Lafond
