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 (12 séances 1h30) + TD (9 séances de 3h00)
• Partiel + Examen final (seule une feuille A4 manuscripte recto-verso sera autorisée aux examens)

Planning

• Cours : lundi 12 septembre 13h30-15h00 et 15h15 et 16h45 puis mercredi 9h00-10h30 (toutes les semaines à partir du 15 septembre)
• TD début semaine du 19 septembre
  • Mardi 13h30-16h45, D101 : Groupe 1, E212 : Groupe 4
  • Jeudi 13h30-16h45, D201 : Groupe 2,
  • Vendredi 13h30-16h45, D203 : Groupe 3-MIAGE,

• Partiel semaine 24 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é
• Examen session 1 : semaine du 12 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 session 2 :
  • Examen 2012
  • Examen 2013
  • Examen 2014
  • Examen 2015

3  Plan

• Introduction
• Introduction au langage logique
  • TD 1 : langage logique
• Logique propositionnelle classique
  • Sémantique
    • TD 2 : Calcul Propositionnel (1)
  • Mises en forme normales
    • TD 3 : Calcul Propositionnel (2)
  • Preuves : Système G et résolution
    • TD 4 : Preuves système G)
    • Memento: règles du système G
    • TD 5 : Preuves sat-solver et résolution
• Calcul des prédicats
  • Syntaxe
    • TD 6 : Syntaxe et sémantique du calcul des prédicats
  • Sémantique
    • TD 7 : Sémantique du calcul des prédicats
  • Equivalences
    • TD 8 : Calcul des prédicats : skolémisation et modèle de Herbrand
  • Preuves

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