Automated Reasoning

A.Y. 2021/2022
Overall hours
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.
Course syllabus and organization

Single session

Lesson period
Second semester
Course syllabus
Resolution calculus, Herbrand theorem, completeness via lifting lemma; reduction orderings, Knuth-Bendix algorithm and superposition calculus.
DPLL and DPLL(T) with heuristics; combination and examples of decision procedures.
Groebner bases and Buchberger algorithm.
Quantifier elimination in numerical domains.
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
Educational website(s)