1. Home
  2. Education
  3. Degree programme courses
  4. Automated Reasoning

Automated Reasoning

A.Y. 2024/2025
6
Max ECTS
52
Overall hours
SSD
MAT/01
Language
Italian
Learning objectives
We shall introduce the main technologies employed in automated reasoning, based both on saturation and on backtracking methods. Applications covering computational algebra topics as well as formal verification problems will be considered. The student will be introduced to some state-of-the-art tools, like SAT- and SMT-solvers, superposition provers, finite and infinite state model checkers.
Expected learning outcomes
To be acquainted with automated reasoning tools (SMT-solvers and superposition provers), from the point of view both of practical use and of theoretical foundations.

Lesson period: Second semester

Lessons timetable

Exams calendar

Single course

This course can be attended as a single course.

Take a single course
Course syllabus and organization

Single session

Responsible
Ghilardi Silvio
Lesson period
Second semester
Course syllabus
Resolution calculus, Herbrand theorem, completeness via lifting lemma; reduction orderings, Knuth-Bendix algorithm and superposition calculus. Completeness of the superposition calculus via model generation.
DPLL and DPLL(T) with heuristics; combination and examples of decision procedures.
Abstract rewrite systems, applications to computer algebra.
Prerequisites for admission
The logic part does not have special prerequisites; the computational algebra part requires elementary abstract algebra knowledge.
Teaching methods
Standard lectures and lab activities on dedicated tools.
Teaching Resources
Electronic notes (available in Ariel)
Software: tools SPASS and z3
Assessment methods and Criteria
Lab activities will take place during the course (students are supposed to take part to them, although they won't contribute to the final evaluation); the exam will consist of an oral colloquium.
MAT/01 - MATHEMATICAL LOGIC - University credits: 6
Practicals: 12 hours
Laboratories: 12 hours
Lessons: 28 hours
Professor: Ghilardi Silvio
Shifts:
Turno
Professor: Ghilardi Silvio
Professor(s)