Information about the course Automated Reasoning (NWI-IMC009)

This course will be given in the fall of 2019, in the first semester.
The first five lectures are roughly covered by the MOOC available at https://www.coursera.org/learn/automated-reasoning-sat, where this material has been split up into 21 professionally recorded lectures of around 10 minutes. After registration by entering name and email address, these MOOC lectures are accessible for free.

Teacher: Prof Dr H. Zantema, Mercator 1, room 1.16 (only on Tuesday), h.zantema@tue.nl

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: October 29, 2019 for the first part, and December 17, 2019 for the second part.
The reports of the practical assignment should be handed in via Brightspace.


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:


Some of the material of the course is based on the books:

S. N. Burris:
Logic for Mathematics and Computer Science
Prentice Hall, 1998, ISBN 0-13-285974-2

C. Meinel and T. Theobald:
Algorithms and Data Structures in VLSI Design
Springer, 1998, ISBN 3-540-64486-5

Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest and Clifford Stein:
Introduction to Algorithms
MIT Press, 2009, ISBN 978-0-262-53305-8
Third Edition, only Chapter 29


Lectures and topics (updated after every lecture):


date topic slides
September 3 Overview, pigeon hole formula, SAT is NP-complete, arithmetic (addition and multiplication) in SAT 1 to 37
September 10 Program correctness by SAT, resolution, Davis-Putnam procedure, completeness of resolution 38 to 69
September 17 DPLL, conflict driven clause learning, dimacs format, SMT syntax 70 to 95, 176-183
September 24 Tseitin transformation, 8 queens, linear programming: simplex method 96 to 152
October 1 Linear programming: simplex method, SMT solving, ILP is NP-complete, model checking / transition systems 153 to 188
October 8 Model checking, CTL, deadlock detection in hardware 189 to 232
October 15 NuSMV, unique representation, decision trees, BDDs 233 to 280
November 5 BDDs, predicate logic 281 to 324
November 12 Predicate logic, resolution, unification
November 19 Unification, resolution, Prolog
November 26 Prenex normal form, Skolemization, Prover9, equational reasoning
December 3 Term rewriting: main properties, termination, well-founded induction, Newman's Lemma
December 10 Term rewriting: critical pairs, word problem, Knuth-Bendix completion
December 17 Knuth-Bendix completion, overview course, old exam (last lecture)



Last change: November 7, 2019