Logique 1

Logique 1Code de l'UE : HLIN402

Présentation

L'UE de logique 1 s'intéresse à la formalisation du raisonnement et aux méthodes de résolution de problèmes logiques.
Cette UE étudie pour l'essentiel les propriétés des connecteurs logiques entre proposition, l'accent est donc mis sur
la logique des propositions . Une introduction à la logique des prédicats sans symbole de fonction est proposée en fin
d'UE.

Programme :

  • Initiation aux raisonnements logiques
  • Syntaxe de la logique des propositions
  • Sémantique de la logique des propositions : interprétations et modèles
  • Définitions des "problèmes" posés en logique et étude des liens entre eux : satisfiabilité, validité, équivalence, conséquence
  • Modélisation en logique des propositions
  • Méthodes de preuve : résolution, tableaux sémantiques, procédure de Davis et Putnam
  • Introduction à la logique des prédicats (sans symbole de fonctions) : syntaxe, sémantique, modélisation

Cette UE s'appuie sur des Cours et TDs mais aussi sur des TPs en salle machine pour implanter les raisonnements
étudiés.

 

Objectifs

L'objectif de cette UE est d'acquérir les bases de la formalisation logique des raisonnements que ce soit dans un
objectif de rédaction de preuves mathématiques ou de mise en place de systèmes de raisonnement automatique.

  • D'un point de vue modélisation, l'objectif est d'être capable de formaliser un problème de raisonnement dans le formalisme logique et à l'inverse de "comprendre" une formule logique pour laquelle une interprétation intuitive des symboles non logiques est donnée.
  • D'un point de vue preuve, l'objectif est d'être capable de rédiger des preuves (directe, par l'absurde, par induction...).
  • D'un point de vue raisonnement automatique, l'objectif est de se familiariser avec les différentes techniques de résolution des problèmes logiques et d'être capable de les implanter dans un langage informatique.




Conditions d'admission

On suppose acquises les notions mathématiques de construction inductive, définition inductive d'une fonction
et preuve par induction structurelle (ou au minimum les notions de définition et raisonnement par récurrence)
et la notion algorithmique associée de récursivité.

Par ailleurs, pour la partie TP, on suppose acquises les notions de base de l'algorithmique et la maîtrise d'un
langage de programmation. Les TPs sont prévus pour être réalisés dans un langage fonctionnel interprété par
exemple : Caml, Lisp, Scheme, Maple...)

Les cours de L1 "Fondements de l'informatique" et "Introduction à l'algorithmique et à la programmation" permettent
d'acquérir ces prérequis.

Volume horaire

  • CM : 15
  • TD : 21
  • TP : 13.5

Syllabus

  • N.H. Xuong : Mathématiques discrètes et informatique - MASSON
  • P. Gochet et P. Gribomont : Logique : méthodes pour l'informatique fondamentale - Hermès
  • R. Lassaigne, M. de Rougemont : Logique et fondements de l'informatique - Hermès
  • M. Bernardet : Introduction pratique aux logiques classiques (exos corrigés) - Hermann
  • R. David, K. Nour, C. Raffalli : Introduction à la logique : Théorie de la démonstration - Dunod
  • S. Russel, P. Norvig : Artificial Intelligence : A Modern Approach (chapitres 7, 8 et 9) cf. AIMA sur le web (il existe également une traduction en français de F. Popineau, L. Miclet, A. Reutenauer? aux éditions Pearson)


Diplômes intégrant cette UE

En bref

Crédits ECTS 5

Nombre d'heures 49 HE

Période de l'année
S4

Langue d'enseignement
fr

Contact(s)

Composante

Contact(s) administratif(s)

Michel LECLERE (michel.leclere @ umontpellier.fr)