Automated Reasoning
A.Y. 2019/2020
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
Single course
This course cannot be attended as a single course. Please check our list of single courses to find the ones available for enrolment.
Course syllabus and organization
Single session
Responsible
Lesson period
Second semester
Course syllabus
- 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.
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.
Prerequisites for admission
No specific preliminary knowledge is required
Teaching methods
Standard lectures and lab classes
Teaching Resources
Electronic notes will be available from Ariel website; specific tools (superposition provers, SMT-solvers, model checkers) will be used, the related links will be shown in the Ariel website. The tools are freely available for non commercial purposes.
Assessment methods and Criteria
The final examination consists of an oral exam. In the oral exam, the student will be required to illustrate results and applications presented during the course in order to evaluate her/his knowledge and comprehension of the arguments covered as well as the capacity to apply them. The evaluation will take into account also the partecipation to lab classes.
Final marks are given using the numerical range 0-30, and will be communicated immediately after the oral examination.
Final marks are given using the numerical range 0-30, and will be communicated immediately after the oral examination.
MAT/01 - MATHEMATICAL LOGIC - University credits: 6
Practicals: 10 hours
Laboratories: 12 hours
Lessons: 28 hours
Laboratories: 12 hours
Lessons: 28 hours
Professor:
Ghilardi Silvio
Shifts:
-
Professor:
Ghilardi SilvioProfessor(s)