Mathématiques pour l’informatique 2
Responsable: Christine Paulin-Mohring
(
paulin@lri.fr
)
TD : François Gonard, Véronique Ventos
TP : Stefania Dumbrava
http://www.lri.fr/ paulin/MathInfo2
2015–16
Nouvelles
TP noté, mardi 12 avril 13h30-16h salles 213 et 214
Devoir Coq à rendre le lundi 11 avril 2016.
Début vendredi 22 janvier 2016 : cours de 8h15 à 10h15 et TD de 10h30 à 12h30
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 (10 séances 2h00) + 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
Devoir Coq
noté
à rendre avant le
lundi 11 avril minuit
Enoncé
,
Squelette
Devoir 2014-2015
Enoncé
TP Coq noté mardi 12 avril
Planning
Cours, début vendredi 22 janvier 2015, de 8h15 à 10h15
salle 109, bât 336
puis le jeudi de 10h30 à 12h30
amphi H1, bât 333
TD début 22 janvier
Groupe 2, vendredi 10h30-12h30, salle 107, V. Ventos
Groupe 3
vendredi 10h30-12h30, salle 034, F. Gonard (sauf 12 février, 4 mars et 1er avril)
mardi 13h30-15h30, salle 034, les 9 février, 1er mars et 29 mars
Vacances d’hiver du 22 au 28 février 2016
Partiel (2h) : semaine du 8 mars (feuille manuscripte recto-verso autorisée)
Partiel 2014-15 + corrigé
TP noté groupes 2 et 3
Mardi 12 avril 2016 13h30-16h00
salles 213 et 214
Dernier cours jeudi 7 avril 2016
Vacances de printemps : du 25 avril au 1 mai 2016
Examen session 1 : prévu le 19 mai matin (feuille manuscripte recto-verso autorisée)
Examen 2014-15 session 1
Examen session 2 : prévu le 14 juin après-midi
Examen 2014-15 session 2
Travaux Pratiques
Preuves sur ordinateur avec un assistant à la démonstration :
Coq
groupe 2, salle 314 : mardi 14h-16h30 les 9 février, 1 mars et 29 mars
groupe 3, salle Nautilus B : vendredi 10h-12h30 les 12 février, 4 mars et 1er avril
groupes 2+3, salles 213 et 214 : mardi 12 avril 13h30-16h00
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 avant le 11 avril 2016
TP noté
mardi 12 avril
(les 2 groupes) guide Coq et TP autorisés.
3 Plan
Notes du cours (version provisoire, jan 2016)
Table des matières
Introduction
Le cadre logique
TD 1
Graphes
TD 2
(preuves, graphes)
TD 3
(graphes, chemin)
TD 4
(graphes, récurrence)
Système d’inférence, induction, récursion
TD 5
(définition par clôture, définitions récursives)
Le paysage syntaxique
TD 6
(définitions récursives, mots, arbres)
Équivalences et Ordres
TD 7
(termes, équivalence)
Calcul propositionnel
TD 8
(ordres bien fondés, algèbre de Boole)
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
A
T
E
X par
H
E
V
E
A