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

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 un minimum d’objets mathématiques utilisés en informatique.

2  Organisation

Evaluation

• Cours (13 séances 1h30) + TD (13 séances de 2h00)
• Partiel + Examen final (seule une feuille A4 manuscripte recto-verso sera autorisée aux examens)

Planning

• Cours : mercredi 8h30-10h00 (toutes les semaines à partir du 6 septembre)
• TD
  • Mercredi 10h15-12h15, B107 : Groupe 1
  • Mercredi 15h15-17h15, B107 : Groupe 2
  • Jeudi 10h15-12h15, B107 : Groupe 3
  • Jeudi 10h15-12h15, B109 : Groupe 4 (MIAGE)

• Partiel semaine 23 octobre (feuille manuscripte recto-verso autorisée)
  • Enoncé partiel 2012 avec corrigé
  • Enoncé partiel 2013 avec corrigé
  • Enoncé partiel 2014 avec corrigé
  • Enoncé partiel 2015 avec corrigé
  • Enoncé partiel 2016 avec corrigé
  • Enoncé partiel 2017 avec corrigé
  • Enoncé partiel 2018 avec corrigé-Correction des questions du qcm
• Examen session 1 : semaine du 18 décembre (feuille manuscripte recto-verso autorisée)
  • Examen 2012 avec corrigé
  • Examen 2013 avec corrigé
  • Examen 2014 avec corrigé
  • Examen 2015 avec corrigé partiel
  • Examen 2016
  • Examen 2017
• Examen session 2 :
  • Examen 2012
  • Examen 2013
  • Examen 2014
  • Examen 2015
  • Examen 2016

3  Plan

• Introduction
  • TD 1 : langage logique
  • TD 2 : langage logique
  • TD 3 : langage logique
• Introduction au langage logique
• Logique propositionnelle classique
  • Sémantique
  • Mises en forme normales
    • TD 4 : Formes normales
  • Preuves : Système G et résolution
    • Memento: règles du système G
    • TD 5 : Calcul des séquents
    • TD 6 : Résolution et satisfiabilité
    • TD 7 : Sudoku
    • Exercices de révision
• Calcul des prédicats
  • Syntaxe
  • Sémantique
    • TD 8 : Syntaxe et sémantique du calcul des prédicats
  • Equivalences
    • TD 9 : Calcul des prédicats : skolémisation et modèle de Herbrand
  • Preuves
    • TD 10 : Calcul des prédicats : unification
    • TD 11 : Calcul des prédicats : résolution

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. La logique. Le Pommier, 2015.

[6]

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