L'objectif du cours est de se familiariser avec le formalisme de la logique du premier ordre. La logique est utilisée pour modéliser des problèmes informatiques et comme outil de spécification de contraintes sur des objets informatiques comme des bases de données ou des programmes. Ce cours aborde les notions de démonstration, de validité, le lien entre les objets physiques (syntaxe) et le sens qu'on leur donne (sémantique). Il présente plusieurs techniques de démonstration automatique comme le calcul des séquents et la résolution. Il met en pratique un certain nombre d'outils mathématiques utilisés en informatique, comme les définitions récursives de fonctions, les preuves par récurrence structurelle ou les définitions par règle d'inférence.
Les soutiens sont par groupes de 2h. |
| Module: | L3 Informatique-S5 |
| |
| 1 * 18 h | Cours | Christine Paulin(1) |
| 4 * 24 h | TD | Aquilina Khoury(1) Nathan Thomasset(1) Marin Costes(1) Thiago Felicissimo(22h) Louise Dubois de Prisque(2h) |
| 1 * 1 h | Soutien-TD | Monsieur TMP(1)[GRAT] |
| 1 * 1 h | Soutien Session-2 | Christine Paulin(3) Monsieur TMP(-2)[GRAT] |
42 h présentielles (hors soutien) |
| |
|
| Un groupe LDD-InfoMath et un groupe Magistère. |
| Module: | LDD3 Informatique et Mathématiques-S5 |
| |
| 1 * 6 h | Cours | Christine Paulin(1) |
| 2 * 18 h | TD | Christine Paulin(1) Pas-Cette Annee(1)[GRAT] |
42 h présentielles (hors soutien) |
| |
|
| Module: | LDD3 Informatique-S5 (Magistère 1) |
| |
18 h présentielles (hors soutien) |
| |
LDD-L3-S5 - Logique pour l'informatique [sep-dec]