Pas encore de diplôme affecté
Logique et Intelligence Artificielle
Code apogéeDIFO5INAStructurexxDernière mise à jour le04 Juillet 2017
Responsable pédagogiqueMASSE Damien (Maître de conférences, 27ème section)
Intervenants
Parcours
    TypeObligatoire
    Semestre5Volume horaire60Crédits ECTS6.5
    Nombre d'heures Cours magistraux (CM)24 Travaux dirigés (TD)18 Travaux pratiques (TP)18 
    Pré-requis

    Informatique théorique (S4): induction, logique des propositions.

    Co-requis 
    Objectif Terminal

     Partie logique:

    • Notions de logique formelle : qu'est-ce qu'un syntaxe, qu'une sémantique ? Notions de preuves axiomatiques ou par systèmes de règles, lien entre preuves formelles et sémantique (correction, complétude). Notions de validité et de satisfiabilité.
    • Applications en logique du premier ordre : différence entre variables, fonctions, prédicats. Interprétation des quantificateurs. Notion de théorie et modèle. Notion de théorie avec égalité.
    • Savoir écrire une preuve simple dans un système formel, ou vérifier qu'une preuve est correcte.
    • Savoir que la validité d'une formule en logique du premier ordre en indécidable, mais que la vérification d'une preuve est décidable.

    Partie PLC:

    • Connaître les bases d'un langage de programmation logique.
    • Savoir programmer des algorithmes de base (avec listes, arithmétique, coupure) en programmation logique.
    • Connaître les bases de la programmation par contrainte, et savoir résoudre un problème à l'aide de la programmation par contrainte.
    Objectif Pédagogique 
    Contenu détaillé de l'enseignement
    • Logique du premier ordre (calcul des prédicats) (12h CM, 8h TD, 4h TP)
      • définition, syntaxe, sémantique, validité, satisfiabilité, systèmes de preuves (méthode axiomatique, calcul des séquents)
      • mise en forme prénexe, herbrandisation, skolémisation, théorème de Herbrand, méthodes semi-automatiques (résolution)
      • théories du premier ordre, théories du premier ordre avec égalité
    • Programmation logique avec contraintes (12h CM, 10 h TD, 14h TP)
      • constructions de base, base de données, programmation récursive, unification, résolution
      • langage PLC : liste, arithmétiques, coupure, dif
      • résolution de problèmes : coloriage de cartes, problème des reines, recherche, jeux, compilation...
    Méthodes d'enseignement

    Cours magistraux, TD et TP.

     

    dispensé en anglais dans le parcours international 

    Evaluation session 1

    Un examen de TP de 1h30 (coef 1) et un examen écrit de 2h (coef 1)

    Evaluation session 2Un écrit de 2h
    Références Bibliographiques
    1. F. Fages, Programmation Logique par Contraintes, collection Cours de l\'Ecole Polytechnique, Ellipses, 1996, ISBN 2-7298-4613-1
    2. R. David, K. Nour, C. Raffalli, Introduction à la logique, cours et exercices corrigés, Dunod, 2001, ISBN 2-1000-4892-9
    3. A. Aho, J. Ullman, Concepts fondamentaux de l\'informatique, collection Sciences Sup, Dunod, 1996. ISBN 2-1000-3127-9