Introduction

• Programme officiel
• Objectifs
• Plan
• Préambule

Programme officiel

• Graphes : définition, isomorphisme, degré, chemin, connexité, coloration, graphes planaires
• Arbres
• Ensembles ordonnés : propriétés, majorants, minorants
• Ordre bien fondé, induction
• Treillis et théorème de point fixe
• Définition inductive d’ensembles et relations : système d’inférence, preuve par induction
• Algèbre de Boole : booléens, anneaux de Boole, lois de de Morgan
• Fonctions booléennes : formes normales
• Calcul propositionnel : syntaxe, sémantique, démonstration, complétude
• Calcul propositionnel : démonstration automatique, formes normales, résolution, séquents, satisfiabilité

Objectifs

• Raisonner sur des structures utiles en informatique :
  • graphes, séquences, arbres, ordres
• Savoir utiliser le calcul propositionnel :
  • système de déduction, modèle, représentation des connaissances

Plan

1. Rappels : logique, formalisation en théorie des ensembles
2. Graphes
3. Inférence, induction et récursion
4. Structures séquentielles, arbres
5. Ordres
6. Algèbre de Boole
7. Calcul Propositionnel

Préambule

Les mathématiques sont une science qui s’intéresse à établir des propriétés d’objets abstraits. Il y a plusieurs activités :

• définir les bons objets abstraits sur lesquels raisonner, faire le lien avec les problèmes concrets;
• énoncer des propriétés intéressantes à étudier (générales, pertinentes);
• démontrer des théorèmes c’est-à-dire construire un enchainement de raisonnements élémentaires qui garantissent que si certaines hypothèses sont satisfaites alors la propriété sera vérifiée.

L’activité mathématique passe par l’utilisation d’un langage commun spécifique afin d’éviter les ambiguités du langage naturel. Dans ce langage, on distingue une partie qui sert à décrire les objets, les mathématiciens utilisent courament le langage de la théorie des ensembles et une partie qui sert à décrire les enchainements logiques corrects en utilisant les connecteurs logiques.

Utiliser un langage précis permet également de faire faire des preuves à des machines. Dans ce cours nous aborderons deux classes d’outils. Nous utiliserons en TP un assistant de preuve (Coq) qui propose un langage puissant mais laisse à l’utilisateur la responsabilité d’indiquer les étapes de la preuve, l’ordinateur ne fait que vérifier que le raisonnement est correct. Nous étudierons dans le cours le calcul propositionnel et montrerons comment utiliser l’ordinateur pour démontrer automatiquement ces formules.