Curriculum M1 MPRI at ENS Paris-Saclay

LAIK: Logic for AI: Knowledge Logics

Description: This course focuses on the logical aspects of artificial intelligence, aiming to reason formally about the knowledge held by agents or coalitions of agents. The methods presented in the course are derived from foundations in logic and automata theory, as well as from the model-checking approach used for program verification. Several families of logical formalisms are introduced, including description logics (such as ALC), strategic temporal logics (such as ATL), and similar formalisms.

Outline:

  1. Introduction to description logics.
  2. Semantic properties.
  3. Tableau method and undecidability results.
  4. Introduction to strategic temporal logics.
  5. Model-checking algorithm and introduction to extensions.
  6. Complexity and the extension with resources.


References:

  • F. Baader et al. An Introduction to Description Logic. Cambridge University Press, 2017
  • S. Demri. Concise Introduction to Alternating-Time Temporal Logics, Springer 2026.
  • Web site of instructors ...