Automated reasoning
[INGI2264]
[30h + 15h] 5 crédits
Cette activité se déroule pendant le 1er quadrimestre.
Enseignants : Charles Pecheur
Langue d'enseignement : Anglais
Niveau : Second cycle
Objectifs (en termes de compétences)
- Comprendre et décrire les techniques de bases ainsi que les bases théoriques utilisées en raisonnement automatisé.
- Comprendre et maîtriser les avantages respectifs des différentes formes de logiques, notamment pour leur utilisation dans le raisonnement automatisé.
- Appliquer à bon escient les techniques et méthodes de raisonnements automatisés
- Comprendre et utiliser les systèmes de raisonnements automatisés existants et représentatifs.
- Développer des applications basées sur l'utilisation de méthodes de raisonnements automatisés.
Objet de l'activité (principaux thèmes à aborder)
- Raisonnements basés sur la logique des propositions : model generation, Davis Putnam, ...
- Raisonnements basés sur la logique classique : résolution, méthodes des tableaux, ...
- Raisonnement avec théorie de l'égalité : paramodulation, unification. réécriture, ...
- Raisonnement basés sur l'induction
- Raisonnements basés sur des logiques non classiques : théorie des types, unification d'ordre supérieure, matching, logiques non monotones, logique multivaluée, logique temporelle, ...
- Systèmes existants de raisonnements automatisés : HOL, Isabelle, KIV, PVS, B, Otter, Nuprl, ...
- Applications : modélisation et résolution de problèmes en utilisant des méthodes de raisonnements automatisés.
Résumé : Contenu et Méthodes
Autres informations (Pré-requis, Evaluation, Support, ...)
INGI21261 Artificial Intelligence : Knowledge and Representation
Ouvrages de référence :
- Kelly, J. (1997), The Essence of Logic. Prentice Hall.
- Alan Robinson , Andrei Voronkov (Editor): Handbook of Automated Reasoning (Vol 1 & 2), MIT Pres, 2001.