AccueilLicence généraleInformatiqueEnseignementsLogique

Licence InformatiqueUE Logique

Contenu

Cette unité d'enseignement a pour objectif de raisonner sur les formalismes logiques au cœur des mathématiques et de l'informatique. Des systèmes formels de déduction sont étudiés, tant pour aider à mieux prouver manuellement des théorèmes que pour comprendre comment automatiser les preuves.

Calcul propositionnel

  • syntaxe et sémantique
  • modélisation par SAT et algorithmes pour SAT (et ses variantes)
  • preuves formelles : séquents, résolution, déduction naturelle
  • compacité

Calcul des prédicats

  • syntaxe et sémantique
  • modélisation
  • formes normales, skolémisation
  • preuves formelles : séquents, résolution

Compétences visées

  • Se servir aisément des bases de la logique pour valider ou réfuter un raisonnement.
  • Rédiger de manière synthétique et rigoureuse des preuves.
  • Utiliser les concepts fondamentaux de l'informatique (langages formels, logique, et graphes) pour la programmation et la modélisation.

Langue utilisée

Langue principale utilisée par cet enseignement : Français.

Bibliographie

  • Logique Mahématique (tome 1), Cori & Lascar, ed. Dunod.

Pré-requis recommandés

  • Structures discrètes

Modalités d'organisation

Les TD se font en autonomie : les étudiants travaillent par groupe de quatre sur les exercices. Il est attendu d’eux qu’ils échangent pour parvenir à la solution. L’enseignant circule de groupe en groupe pour répondre aux questions qui se posent. Ce dispositif suppose l’accès à une salle dotée de tables amovibles et de plusieurs tableaux.

Volume des enseignements

  • Cours magistraux : 20 heures
  • Travaux dirigés : 30 heures
  • Travaux pratiques : 10 heures

Les formations qui utilisent cet enseignement