Automated reasoning [ LINGI2264 ]

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.

Pas donné en 2013-2014

• 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