Descriptif

La capacité de raisonner automatiquement sur des formules logiques est cruciale pour résoudre des problèmes en Intelligence Artificielle (par exemple, la planification de chemins et de tâches) et en Méthodes Formelles (par exemple, la vérification de logiciels). Ce cours présentera les algorithmes modernes et efficaces (procédures de décision) utilisés pour vérifier la satisfiabilité (SAT) de formules en logique propositionnelle (par exemple, l'apprentissage par conflits avec clauses, CDCL) et les extensions de ces algorithmes pour vérifier des formules en logique du premier ordre plus expressives (Satisfiabilité Modulo Théorie, SMT). Le cours présentera également comment la modélisation logique et la satisfiabilité peuvent résoudre des problèmes en IA (agent basé sur la connaissance logique) et en méthodes formelles (vérification de logiciels). En détail, le tutoriel abordera des problèmes tels que la planification de chemins, la planification de tâches et la vérification de modèles bornés pour illustrer les notions théoriques et la mise en œuvre pratique des algorithmes.