Information about the course Automated Reasoning (NWI-IMC009)

Teacher: Prof Dr H. Zantema, h.zantema@tue.nl

This course will be given in the fall of 2021, in the first semester.

The course will be offered partly on campus, on Tuesday, 13:30, with roughly one lecture in two weeks, starting at September 7, see schedule below. In between there will be online meetings in Brightspace Virtual Classroom, also on Tuesday, 13:30. Please watch the corresponding recorded lectures before these meetings.
The full series of recorded lectures from 2020 is available and up to date. They are numbered, please follow them no later than indicated in the schedule below. The physical lectures will cover roughly two of these recorded lectures each.

You may always ask questions to h.zantema@tue.nl.

The first eight lectures are roughly covered by the MOOC available at https://www.coursera.org/learn/automated-reasoning-sat and https://www.coursera.org/learn/automated-reasoning-symbolic-model-checking, where this material has been split up into several professionally recorded lectures of around 10 minutes. After registration by entering name and email address, these MOOC lectures are accessible for free.

Goal:
Obtaining insight how various problems can be transformed to formulas, and can be solved automatically by computer programs manipulating these formulas.


Contents:
Many problems, in particular in the area of verification of computer systems, can be expressed as proving that some big formula is always true. In this course we will concentrate on various methods for treating this kind of problems. Not only correctness and completeness of these methods will be considered, also efficiency and usability. In particular we will consider:



Examination:
The examination consists of two parts: a written exam and a practical assignment. The written exam is `closed book': no use of books or notes is permitted during the exam. The practical assignment is done by at most two persons. In case the practical assignment is done by two persons, each of them should be responsible for the whole work, possibly checked by an individual test. The practical assignment has two deadlines: November 2, 2021 for the first part, and January 5, 2022 for the second part.
The reports of the practical assignment should be handed in via Brightspace. If you do it with two people, only one of them should submit.


For both the written exam and the practical assignment, the grade should be at least 5.0. In that case the final grade is the average of both parts, each having the same weight. Otherwise the final grade is the minimum of both parts.


To be downloaded:


lecture date topic slides
Nr 01 September 7 (lecture on campus) Overview, pigeon hole formula, SAT is NP-complete, arithmetic (addition and multiplication) in SAT 1 to 40
Nr 02 September 14 (lecture online) Program correctness by SAT, resolution, Davis-Putnam procedure, completeness of resolution 41 to 73
Nr 03 September 21 (lecture online) DPLL, conflict driven clause learning, dimacs format, Tseitin transformation 74 to 107
Nr 04 September 28 (lecture on campus) 8 queens problem, linear programming: simplex method 108 to 150
Nr 05 October 5 (lecture online) Linear programming: simplex method, SMT solving, ILP is NP-complete 151 to 187
Nr 06 October 12 (lecture on campus) Model checking, NuSMV, CTL 188 to 228
Nr 07 October 19 (lecture online) Deadlock detection in hardware, unique representation of boolean functions, decision trees 229 to 256
Nr 08 November 9 (lecture on campus) Decision trees, BDDs 257 to 314
Nr 09 November 16 (lecture online) BDDs, Predicate logic, resolution, unification 315 to 344
Nr 10 November 23 (lecture on campus) Unification, resolution, Prolog, Prenex normal form, Skolemization 345 to 366
Nr 11 November 30 (lecture online) Prover9, Equational reasoning, term rewriting, main properties, termination 367 to 387
Nr 12 December 7 (lecture on campus) Term rewriting: monotonic interpretations, lpo, dependency pairs, well-founded induction, Newman's Lemma 388 to 414
Nr 13 December 14 (lecture online) Critical pairs, word problem, Knuth-Bendix completion, overview course 415 to 435
December 21 (opportunity to ask questions online) Presentation of examination April, 2020



Last change: January 25, 2022