Teachers: Sylvain Conchon (LRI, Univ. Paris-Saclay) & Stéphane Demri (LSV, ENS Paris-Saclay)

This course 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 course proposes a large overview of logical formalisms related to AI issues.

Sessions will take place in room C315 (Cournot building, ENS Paris-Saclay, Cachan) on Mondays from 14:00 to 18:30, starting on November 18th.

Exam on the second part will take place on January 13th, 2020 from 2pm to 4pm, room C315. The only allowed documents are the slides of the lectures in printed paper (no device).

The first part of the courses (lectures on 18/11/19, 25/11/19, 02/12/19) is dedicated to the problems SAT and SMT (Satisfiability Modulo Theory). Here is a brief description:

• Problem SAT, algorithm DPLL
• Learning, back jump, algorithm CDCL
• Problem SMT, naive algorithm
• Examples of theories and related decision procedures : Difference logic (Floyd algorithm), Linear arithmetic on rational numbers (simplex algorithm, Fourier-Motzkin elimination), Equality theory (Union-Find structure, congruence closure)
• Combination of decision procedures: Nelson-Oppen algorithm, Shostak method
• Algorithm CDCL(T)
• Modern SMT techniques: splitting on demand, delayed theory combination, MCSAT

Practice : implementation of a mini SMT-solver

The second part of the course (lectures on 09/12/2019, 16/12/2019, 06/01/20) is dedicated to an introduction of description logics (2 lectures) and on temporal logics to reason about multi-agent systems (1 lecture). Here is a brief description:

• Introduction to description logics: knowledge representation, logical formalisms, introduction to the basic description logic ALC, extensions
• Tableaux methods: tableaux-style proof system for ALC decision problems, extensions
• Computational complexity: complexity of concept satisfiability for ALC, knowledge base consistency for ALC, undecidable problems for ALC extensions
• Introduction to temporal logics for multi-agent systems: concurrent game structures, logics ATL, ATL* and variants, model-checking, extension with ressources and variant with incomplete information (if time permits).

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

Material

Slides for the lecture on 09/12/2019 Exercises Sheet for the session on 09/12/2019

Slides for the lecture on 16/12/2019 Exercises Sheet for the session on 16/12/2019

Slides for the lecture on 06/01/2020 Exercises Sheet for the session on 06/01/2020

Exam on 13/01/2020 Solutions (in French)