Objectifs 

L’objectif de cette UE est de présenter un langage logique (la logique des prédicats), des méthodes de raisonnement formel, des outils et quelques applications associées suivant le type du raisonnement recherché.

Mots-clés :
logique des prédicats, déduction, abduction, induction
Pré-réquis
Bases de la logique (syntaxe et sémantique de la logique propositionnelle, méthodes de preuve en logique propositionnelle)

Description

  1. Introduction :
    • qu'est-ce que le raisonnement formel ?
      • question du langage et notion d'expressivité
      • question de l'inférence et notion de calculabilité
    • typologie des différents types de raisonnement en logique (déduction, abduction, induction)
  2. Logique des prédicats :
    • syntaxe et sémantique, formalisation
    • théorie des modèles
    • théorie de la preuve (séquents de Gentzen)
    • résolution (skolémisation, clauses, unifieur, résolvante)
    • méta-propriétés de la logique des prédicats
    • théories du premier ordre
    • un exemple : la logique équationnelle et son application à la sécurité
  3. Extensions de la logique des prédicats suivant le type de raisonnement recherché :
    • raisonnement déductif avec application :
      • au raisonnement non-monotone, aux techniques de complétion, à la logique des défauts
      • au raisonnement en présence d'inconsistance (restauration de cohérence, approche argumentative et logiques para-consistantes)
    • raisonnement abductif avec application à un problème de diagnostic et présentation d'un outil pour le raisonnement abductif (ATMS)
    • raisonnement inductif et sa formulation logique

Bibliographie :

Mise à niveau Parties 1 et 2 :
  • Cours en ligne : https://www.irit.fr/~Andreas.Herzig/C/
  • Eléments de logique contemporaine avec exercices et corrigés, François Lepage, Presses Universitaires de Montréal (présent à la BU)
  • La logique ou l'art de raisonner, Yannis Delmas-Rigoutsos, René Lallement, éditions Le Pommier (présent à la BU)
Approfondissement Parties 1 et 2 :
  • An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, Andrews P.B., Applied Logic Series , Vol. 27, Springer
Pour la partie 3 :
  • Consequence finding algorithms. In Handbook of defeasible reasoning and uncertainty management systems, Pierre Marquis, (Gabbay & Smets Edts). Vol5. Kluwer Academic Publisher
  • Nonmonotonic reasoning: an overview, Brewke, Dix, Konolige, CLSI Publications, Stanford University, 1997
Equipe pédagogique :
Claudette Cayrol, Yannick Chevalier, Laurence Cholvy, Olivier Gasquet, Andreas Herzig, Marie-Christine Lagasquie
Responsable :
Marie-Christine LAGASQUIE ( Cette adresse email est protégée contre les robots des spammeurs, vous devez activer Javascript pour la voir. ) 05 61 55 64 51