2021/2022

2021/2022

DM270

INF/01 (INFORMATICA)

DIPARTIMENTO DI MATEMATICA 'FELICE CASORATI'

ARTIFICIAL INTELLIGENCE

PERCORSO COMUNE

1°

Primo Semestre (04/10/2021 - 14/01/2022)

6

52 ore di attività frontale

INGLESE

SCRITTO E ORALE CONGIUNTI

GHILARDI SILVIO (titolare) - 6 CFU

The course is basic, no special prerequisites are assumed, beyond generic high school level skills.

During the course, students need to acquire the capability of formalizing various kinds of problems (constraint satisfaction problems, planning problems, verification tasks) using symbolic logic language. They are supposed also to learn how to solve such problems by running appropriate tools like SMT solvers. At the same time, they will acquire information about the theoretical foundations of DPLL procedure and its extension modulo theories.

Propositional logic, truth tables, SAT problems.
Resolution Calculus.
DPLL procedure, with heuristics
(backjumping, learning); DIMACS standard.
First order languages, Tarski semantics. Ground resolution and Herbrand theorem.
DPLL modulo theories; congruence closure, other examples of decision procedures. Combination of decision procedures. SMT-LIB2 standard. Applications to verification and planning. A Python interface for Z3.

The course will alternate traditional lectures and computer activities. Theoretical foundations will be carefully explained by the teacher, using both slides and blackboard. During lab classes, students will be supposed to be able to formalize problems, translate them into common standards (DIMACS, SMT-LIB2) and finally run the specification files using the Z3 solver.

Teachers notes are in preparation and will be ready for the course.
Comprehensive textbook:
Aaron R. Bradley, Zohar Manna"The Calculus of Computation", Springer 2007.

Comprehensive examination, including:
- questions in quiz style;
- questions concerning theoretical foundations;
- exercises aiming at verifying the familiarity with logical calculi and algorithms;
- exercises requiring the production of executable files in the SMT-LIB2 standard;
- oral examination (if needed in order to adjust the final score)