Teachers: Stéphane Demri (LMF, ENS Paris-Saclay) & Mihaela Sighireanu (LMF, ENS Paris-Saclay)

This module presents the logical aspects of AI that are known to be essential to reason formally and symbolically on logical theories and for knowledge representation. Along the years, the logical aspects of AI had their own pace of development, in parallel to what has been done in formal logic. New scientific questions have been raised and this topic is currently at the crossroads of AI and logic, with its own research agenda. A lot of efforts have been devoted to the formalisation of concepts, some of them coming from the philosophical aspects of AI. The necessity to build bridges between several areas such as formal verification or automated deduction, has also been a driving force to develop this subject. This module proposes a large overview of logical formalisms related to AI issues.

Sessions will take place in room 1E14 (except on Dec. 14th in room 1E26), ENS Paris-Saclay, Gif-sur-Yvette, on Wednesdays from 14:00 to 18:30, starting on September 14th, 2022. Some sessions will use the lab room 1S53.

The two parts are independent. The validation of each part gives 4 ECTS.

The first part of the module (six lectures from 14/09/22) is dedicated to an introduction of description logics (3 lectures) and on temporal logics to reason about multi-agent systems (3 lectures). No lecture on October 19th 2022. Here is a brief description:

• Introduction to description logics: knowledge representation, logical formalism, introduction to the basic description logic ALC, extensions
• Tableaux methods: tableaux-style proof system for ALC decision problems, extensions
• Introduction to temporal logics for multi-agent systems: concurrent game structures, logics ATL, ATL* and variants, model-checking, extension with resources and variant with incomplete information.

Each session of this part is divided into a lecture (2/3) and an exercises session (1/3).

The evaluation for this part is a written exam, taking place on November 9th, room 1E14 from 2pm to 5pm (or to 6pm for those entitled to have an extra time).

Material:

• Session on 14/09/2022: slides for the lecture and exercises sheet
• Session on 21/09/2022: slides for the lecture and exercises sheet
• Session on 28/09/2022: slides for the lecture and exercises sheet
• Session on 05/10/2022: slides for the lecture and exercises sheet
• Session on 12/10/2022: slides for the lecture and exercises sheet
• Session on 26/10/2022: slides for the lecture and exercises sheet

The second part of the module (six lectures from 16/11/22) is dedicated to decision procedures for SAT and SMT (Satisfiability Modulo Theory) problems. Here is a brief description (more details):

• SAT problem: DPLL and CDCL algorithms
• SMT problem: CDCL(T) algorithm and Z3 API
• Satisfiability problem in theories for: Equality with uninterpreted functions, Linear rational arithmetic, Linear integer arithmetic, bit vectors, arrays and pointers
• Combination of decidable theories: Nelson-Oppen algorithm

Practice:

• coding a SAT solver
• modeling and solving in Prolog and Z3 API

The evaluation for this part at the first session is composed of 50% of project, 50% of written exam. For the second session, the evaluation is a written exam.