Information about the course Automated Reasoning (2IW15)

This course will be given in the fall of 2014, in the second quartile.
Lectures from 2013 are available on video

Teacher: Prof Dr H. Zantema, Metaforum 7.067, tel 2749,

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

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:

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: December 8, 2014 for the first part, and January 12, 2015 for the second part.

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 (tentative; will be updated every week):

date topic slides
Monday, November 11 Overview, pigeon hole formula, SAT is NP-complete, arithmetic in SAT 1 to 36
Wednesday, November 13 Program correctness by SAT, resolution, Davis-Putnam, completeness 37 to 65
Monday, November 18 DPLL, conflict driven clause learning 66 to 87
Wednesday, November 20 Conflict driven clause learning, Tseitin transformation 88 to 106
Monday, November 25 Linear programming: Simplex method 107 to 135
Wednesday, November 27 SMT solving, unique representation, reachability, NuSMV 136 to 161
Monday, December 2 NuSMV, Decision trees and BDDs 162 to 185
Wednesday, December 4 BDDs 186 to 206
Monday, December 9 Predicate logic, resolution, unification 207 to 230
Wednesday, December 11 Unification, resolution, Prolog, prenex normal form 231 to 248
Monday, December 16 Skolemization, equational reasoning, term rewriting 248 to 263
Wednesday, December 18 Term rewriting: main properties, termination undecidable, termination by monotone interpretations 263 to 279
Monday, January 6 Term rewriting: lexicographic path order, Newman's Lemma, critical pairs 280 to 292
Wednesday, January 8 Term rewriting: word problem, Knuth-Bendix completion, overview course (last lecture) 293 to 306

Last change: September 25, 2014