We examine 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 stateof- the-art tools, like for instance SAT- and SMT-solvers, superposition provers, model finders, finite and infinite state model checkers.
At the end of the course the sudent will be able to use basic tools for automated reasoning, like superposition provers (SPASS, Eprover), SMT solvers (Z3, Yices, MathSat) or infinite state model checkers (muZ, nuXmv, MCMT).
- Skolemization and clausal form reduction; unification algorithm and resolution calculus. The refutational completeness theorem. - Orderings and ordering constraints; ordered resolution. - Paramodulation e Superposition. Reduction rules. The architecture of a prover. - Word problems: critical pairs, completion, Knuth-Bendix algorithm. Finite presentations for groups and monoids. Groebner Bases and Buchberger algorithm. - SAT problems; DPLL procedure. Non-chronological backtracking, Conflict Driven Clause Learning and further heuristics. - From SAT to SMT; basic decision procedures. Combination of decision procedures. The SMT-LIB standard. - Applications to infinite state model-checking. Automated verification of properties of sequential programs and of distributed protocols.