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 des notions 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 4 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 21 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é
  • Enoncé partiel 2019 avec corrigé
• Examen session 1 : semaine du 16 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 2018 avec corrigé QCM
• Examen session 2 :
  • Examen 2012
  • Examen 2013
  • Examen 2014
  • Examen 2015
  • Examen 2016
  • Examen 2017
  • Examen 2018 QCM

3  Plan

• Introduction
  • TD 1 : langage logique, révisions calcul propositionnel TD 2 : langage logique, calcul propositionnel
• Introduction au langage logique
• Logique propositionnelle classique
  • Sémantique
    • TD 3 : modèles, Calcul Propositionnel
  • Mises en forme normales
    • TD 4-5 : Formes normales
  • Preuves : Système G et résolution
    • Memento: règles du système G
    • TD 6-7-8 : Calcul des séquents et résolution propositionnelle
      • Corrigé détaillé des exercices 1 à 3
• Calcul des prédicats
  • Syntaxe
  • Sémantique
    • TD 9-10 : Syntaxe et sémantique du calcul des prédicats
  • Equivalences
  • Preuves
    • TD 11-12 : Skolémisation, Modèles de Herbrand, Unification
    • TD 13 : Résolution, Calcul des Séquents et Révisions

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