Eléments de logique pour l’informatique (Info 315)

Responsable: Christine Paulin-Mohring (paulin@lri.fr)
TD : Philippe Chatalic, Christine Paulin et Rebecca Zucchini
http://www.lri.fr/~paulin/Logique

2020–21

1 Objectifs

L’objectif du cours est de se familiariser avec un formalisme logique, la notion de démonstration, de validité, le lien entre syntaxe et sémantique. Ce cours met en pratique des notions mathématiques utilisés en informatique.

2 Organisation

Evaluation

Cours (12 séances 1h30) + TD (12 séances de 2h00)
Contrôle Continu + Partiel + Examen final (seule une feuille A4 manuscripte recto-verso sera autorisée aux examens et au partiel)

Planning

Cours :
- semaine 1, mercredi 9 septembre : 9h00-10h30 (Licence informatique), 10h45-12h15 (LDD Mathématiques-Informatique et magistère informatique)
- semaines suivantes : à distance sur ecampus, leçon à valider avant d’assister au TD
TD (horaires à confirmer)
- Mercredi 10h45-12h45, B107 : Groupe 3 Informatique
- Mercredi 10h00-12h00, Gd amphi : Groupe 5+6 LDD+magistère
- Mercredi 14h00-16h00, B107 : Groupe 4 MIAGE
- Jeudi 13h30-15h30, B107 : Groupe 1 Informatique
- Jeudi 13h30-15h30, E107 : Groupe 2 Informatique

Partiel semaine 21 octobre (feuille manuscripte recto-verso autorisée)
Examen session 1 : semaine du 16 décembre (feuille manuscripte recto-verso autorisée)
Examen session 2 :

3 Plan

4 Programme officiel

Langage logique
Système de règles logiques pour construire des preuves
Termes : signature, preuve par récurrence structurelle, définition récursive de fonctions
Calcul des prédicats : syntaxe, variables libres et liées, sémantique, équivalence
Modèle, modèle de Herbrand
Exemples de théories
Démonstration automatique, formes normales, résolution, séquents

Références

[1]: Serenella Cerrito. Logique pour l’Informatique : une introduction à la déduction automatique. Vuibert Publisher Co, 2008.
[2]: Robert Cori and Daniel Lascar. Logique Mathématique. Axiomes. Masson, 1993.
[3]: René David, Karim Nour, and Christophe Raffalli. Introduction à la Logique, Théorie de la démonstration. Dunod, 2001.
[4]: 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.
[5]: Gilles Dowek. Les démonstrations et les algorithmes. Les éditions de l’Ecole Polytechnique, 2010.
[6]: Gilles Dowek. La logique. Le Pommier, 2015.
[7]: Yannis Delmas-Rigoutsos et René Lalement. La Logique ou l’art de raisonner. Le Pommier, 2000.

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