Mathématiques pour l’informatique 2

Nouvelles

• Premier cours jeudi 22 janvier 2015 de 9h30 à 12h30 (pas de TD)

1  Objectifs

• Apprendre à raisonner sur des structures utiles en informatique avec des outils adaptés :
  • Objets syntaxiques (graphes, mots, listes, arbres, …)
  • Equivalences, ordres
• Connaître le calcul propositionnel : système de déduction, modèle, représentation des connaissances, démonstration automatique

2  Organisation

Evaluation

• Cours (1 séance de 2h30 + 10 séances 1h45) + TD (10 séances de 2h00), TP (4 séances de 2h30)
• Partiel (coeff 6) + Devoirs (coeff 4) + Examen final (coeff 10)
  (seule une feuille A4 manuscripte recto-verso sera autorisée)

Devoirs

1. Devoir Coq noté à rendre avant le mardi 7 avril 12h Enoncé

Planning

• Cours salle 142 : jeudi 11h00-12h45
• TD: jeudi 8h45-10h45
  • Groupe 3, salle 109, T. Balabonski
  • Groupe 2, salle 142, C. Paulin

• Début jeudi 22 janvier 2015, cours de 9h30 à 12h30 (pas de TD)
• Vacances d’hiver du 23 au 27 février 2015
• Partiel (2h) : mardi 10 mars 2015, 9h30 (feuille manuscripte recto-verso autorisée) Partiel 2014-15 + corrigé
• TP noté Mardi 7 avril 2015 après-midi salles
• Dernier cours jeudi 16 avril 2015
• Vacances de printemps : du 27 avril au 1 mai 2015
• Examen session 1 : du 15 au 22 mai 2015 (feuille manuscripte recto-verso autorisée)

Travaux Pratiques

• Preuves sur ordinateur avec un assistant à la démonstration : Coq
• lundi ou mardi après-midi : 9-10 février, 2-3 mars et 30-31 mars
  + TP noté mardi 7 avril (2 groupes)
  • Groupe 2, lundi 13h30-16h00, salle 313 sauf mardi 7 avril 14h00-16h30, salle 226
  • Groupe 3, mardi 14h00-16h30, salle 224
• Documents
  • Guide d’utilisation de Coq
  • sujet TP 1 squelette TP 1
  • sujet TP 2 squelette TP 2
  • sujet TP 3 squelette TP 3
• Devoir noté à rendre
• TP noté mardi 7 avril (les 2 groupes) guide Coq et TP autorisés.

3  Plan

Notes du cours (version provisoire, jan 2015)

1. Table des matières
2. Introduction
3. Le cadre logique
   • TD 1
   • Règles logique
4. Graphes
   • TD 2 (graphes)
   • TD 3 (graphes,chemin)
5. Système d’inférence, induction, récursion
   • TD 4 (récurrence, définition par clôture)
   • TD 5 (définitions récursives)
6. Le paysage syntaxique
   • TD 6 (mots, arbres, termes)
7. Équivalences et Ordres
   • TD 7 (termes, équivalence)
   • TD 8 (ordres)

4  Programme officiel

• Graphes : définition, isomorphisme, degré, chemin, connexité, coloration, graphes planaires
• Ensembles ordonnés : propriétés, majorants, minorants Ordre bien fondé, induction
• Treillis et théorème de point fixe
• Arbres
• 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 Démonstration automatique, formes normales, résolution, séquents, satisfiabilité

5  Liens utiles

• Archives du cours Mathématiques pour l’Informatique (2010-2014)
• Cours de Logique Licence Informatique (L3)

Références

[1]

André Arnold and Irène Guessarian. Mathématiques pour l’informatique. EdiScience. Dunod, 2005.

[2]

Stéphane Devismes, Pascal Lafourcade, and Michel Lévy. Informatique théorique : Logique et démonstration automatique, Introduction à la logique propositionnelle et à la logique du premier ordre. Ellipses, 2012.

[3]

Jacques Vélu. Méthodes mathématiques pour l’informatique. Sciences Sup. Dunod, 2005.

Ce document a été traduit de L^AT_EX par H^EV^EA