Logiques

Description du cours

Une première partie du cours consiste en une introduction à la logique du premier ordre. Des exemples sur des structures simples comme les graphes nous permettrons de définir un modèle d’une formule ou encore d’exprimer une propriété par une formule d’une logique. Nous étudierons le pouvoir d’expression et la décidabilité de fragments de la logique du premier ordre (principalement les classes préfixes). Nous aborderons brièvement la logique du second ordre pour définir des propriétés nécessaires pour le cours comme la connexité et le principe de récurrence. Nous définirons les propriétés de cohérence et de complétude d’une théorie issue d’un système d’axiomes. Nous verrons quelques systèmes d’axiomes comme l’arithmétique de Presburger et celle de Peano. Dans une seconde partie, nous présentons des techniques avancées d’extraction, d’ingénierie et de représentation des connaissances. Cela couvre les applications de logiques de premier ordre, de logiques de description ainsi qu’une perspective sur les aspects temporels. À cette fin, nous étudions par exemple l’algorithme A-priori pour l’extraction de règles d’association. En outre, nous utilisons la méthode des tableaux pour vérifier la consistance des bases de connaissances. Enfin, une troisième partie du cours consiste en une introduction à la logique modale et à la sémantique de Krikpe avec ses axiomes standards (K, D, T, 4, 5). Afin de donner corps aux concepts vus en cours, les travaux pratiques consisteront en l’implémentation d’une structure de Kripke, d’un algorithme de vérification de modèle et de la méthode des tableaux pour la logique modale standard.