COMPUTATIONAL LOGIC
Stampa
Enrollment year
2021/2022
Academic year
2021/2022
Regulations
DM270
Academic discipline
INF/01 (COMPUTER SCIENCE)
Department
DEPARTMENT OF MATHEMATICS "FELICE CASORATI"
Course
ARTIFICIAL INTELLIGENCE
Curriculum
PERCORSO COMUNE
Year of study
Period
1st semester (04/10/2021 - 14/01/2022)
ECTS
6
Lesson hours
52 lesson hours
Language
English
Activity type
WRITTEN AND ORAL TEST
Teacher
GHILARDI SILVIO (titolare) - 6 ECTS
Prerequisites
The course is basic, no special prerequisites are assumed, beyond generic high school level skills.
Learning outcomes
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.
Course contents
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.
Teaching methods
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.
Reccomended or required readings
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.
Assessment methods
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)
Further information
Sustainable development goals - Agenda 2030