Volumes horaires
- CM 18.0
- TD 18.0
Crédits ECTS
Crédits ECTS 2.5
Objectif(s)
Le raisonnement (ou inférence), entendu au sens large, i.e. non
seulement déductif, intervient pratiquement dans toutes les activités
humaines.
Les différentes logiques sont l'outil le plus général pour le formaliser.
Elles en ont abstrait des règles élémentaires et les façons de les
combiner dans des inférences dont le but est de transformer, expliciter, rendre utilisable, expliquer,_l'information contenue dans une certaine situation. Son lien avec l'Informatique est évident puisque cette dernière est aussi une discipline du traitement formel de l'information (via des langages de programmation). La Logique est également un outil formel de modélisation (e.g. dans les systèmes multi-agents, pour la prise des décisions, dans les descriptions du monde en général_).
Les applications de l'inférence en Informatique, en Intelligence
Artificielle et en Mathématique sont devenues très nombreuses : en
spécification/preuve des programmes, comme langage de
programmation, dans la représentation/utilisation des connaissances,
comme assistants (semi-)automatiques dans le raisonnement
mathématique : dans l'obtention/vérification/ structuration des preuves, dans la génération de contre-exemples _ .
L'objectif de ce cours est de présenter et de donner les propriétés
essentielles d'une grande variété de logiques ainsi que des calculs
permettant de raisonner dans ces logiques.
Ces éléments permettent d'analyser les fondements de systèmes
existants, et des améliorations éventuelles, ainsi que d'imaginer de
possibles systèmes futurs.
L'accent est mis sur le pouvoir d'expression des logiques et leur
adéquation à un traitement informatique.
Ce cours donne des fondements permettant d'évaluer et choisir les
logiques utiles dans la formalisation (modélisation) des problèmes
arrivant dans presque tous les domaines de l'informatique actuelle
(Intelligence Artificielle, spécification et preuve des programmes,
ontologies, web sémantique,_) ainsi qu'en Mathématique :
raisonnement assisté par ordinateur.
Contact Mnacho ECHENIM
Contenu(s)
1. Qu'est-ce que l'Intelligence Artificielle ? Un aspect capital de
l'intelligence : l'inférence
2. Preuve, vérification, modèle, contre-exemples. Preuves par ordinateur. Relation de conséquence. Non-conséquence.
3. Logique classique, quelques classes décidables. Subsomption,
généralisation.
4. Principes de programmation en logique avec contraintes.
5. Inférence en présence de l'égalité.
6. Abduction (i.e. découverte d'hypothèses explicatives). Logique du
second ordre.
7. Logiques non-classiques. Logiques modales, sémantique des mondes possibles. Logiques de la connaissance dans les systèmes multi-agents.
8. Logiques temporelles, logiques des instants, des intervalles, temps
discret, arborescent, logiques temps réel.
9. Logiques polyvalentes. Similarité et logique floue.
Pour toutes les logiques non-classiques différents méthodes d'inférence sont présentées : approches directes et par traduction (dans la logique classique).
Prérequis
Néant. Le cours peut être vu comme une continuation du cours de
" Logique pour l'Informatique " de 1A, mais les étudiants ne l'ayant pas
suivi ne devraient pas avoir de difficulté (puisque les sujets traités en 1A sont expliqués en tout détail dans le poly).
Contrôle des connaissances
Des projets en binôme (ou individuels) avec soutenance.
N1=P1
N2=P2 si P1<12
Informations complémentaires
Bibliographie
Polycopié du cours (contenant problèmes avec solutions) et bibliographie spécifique en rapport avec les projets individuels.