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.

Modalités d'évaluation

Session 1 :

• Contrôle continu (CC1) : Le contrôle continu consiste en un devoir à la maison portant sur la partie logique du premier ordre et un rendu des travaux pratiques portant sur la partie logique modale. La part de chaque rendu dans l’évaluation du CC1 est calculée au prorata du volume horaire consacré à chaque partie dans le cour.
• Contrôle terminal (CT1) : Le contrôle terminal consiste en un écrit de 2 heures avec des exercices portant sur les trois parties au prorata du volume horaire consacré à chacune d’elles dans le cours. Les documents ne sont pas autorisés.
• Note finale : la note finale est calculée de la façon suivante : 13 × CC1 + 32 × CT 1.

Session 2 :

• Contrôle terminal (CT2) : Le contrôle terminal consiste en un écrit de 2 heures avec des exercices portant sur les trois parties au prorata du volume horaire consacré à chacune d’elles dans le cours. Les documents ne sont pas autorisés.
• Note finale : la note finale est calculée de la façon suivante : 13 × CC1 + 32 × CT 2.