Automated reasoning [ LINGI2264 ]

> https://www.icampus.ucl.ac.be/claroline/course/index.php?cid=INGI2264

INGI2261 (Artificial intelligence) ou des fondements équivalents en logique et intelligence artificielle

• Raisonnement automatisé
• Raisonnements basés sur la logique des propositions :  generation de modèles, 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, ...
• Applications : modélisation et résolution de problèmes en utilisant des méthodes de raisonnements automatisés.

Les étudiants ayant suivi avec fruit ce cours seront capables de

• décrire les techniques de bases ainsi que les bases théoriques utilisées en raisonnement automatisé.
• expliquer 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
• 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.

Les étudiants auront développé des compétences méthodologiques et opérationnelles.  En particulier, ils auront développé leur capacité à :

• se documenter sur les outils disponibles dans un domaine,
• présenter de manière claire et complète un logiciel,
• décrire une situation, la modéliser et l'analyser en utilisant un outil adéquat.

• Missions et présentation d'un autre outil (50% de la note finale)
• Examen oral (50% de la note finale)

Cours magistral: découvrir les fondements du raisonnement automatisé

• Bases théoriques, les logiques
• Techniques de base, avantages et inconvénients

Labos: appliquer deux outils du raisonnement automatisé

• 2 missions avec Alloy et Maude introduites par des séances en salle
  
• Apprendre à utiliser des outils, développer des applications basées sur les outils

Lecture: découvrir d'autres outils

• Chaque élève en présente un à la classe

• Introduction
  
• Logique propositionnelle
• Diagrammes de décision binaires
• Logique du premier ordre
• Fondements d'Alloy
• Egalité
• Fondements de Maude
• Théories du premier ordre
• Au-delà de la logique du premier ordre

• Pas de livre obligatoire mais de nombreux ouvrages de référence
• Transparents et documents en ligne