Logique et langages

Ce cours introduit la logique des modèles finis, tels que les mots, les arbres et les graphes fini, ainsi que des logiques temporelles utilisées en vérification. Nous présenterons également les logiques de description qui servent à représenter de manière formelle des connaissances d’un domaine particulier (e.g. médecine) pour améliorer l’interrogation et le partage d'informations. On s’intéressera au pouvoir d’expression des logiques considérées, ainsi que des problèmes algorithmiques variés (validation de formule sur un modèle, satisfiabilité de formule, inférence logique, etc).

Nous aborderons également l’apprentissage d'automates et de formules LTL à partir d’exemples dans des contextes passifs et actifs. Nous discuterons des algorithmes associés à ces problèmes (bornes supérieures) ainsi que des questions de complexité (bornes inférieures). Si le temps le permet, nous mettrons également en lumière un lien étroit entre la théorie des automates et la complexité des circuits algébriques, et montrerons comment les résultats de l'une peuvent être appliqués à l'autre.