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.
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.
Standard lectures and lab activities on dedicated tools.
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.