Information about the course Automated Reasoning (2IMF25)

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

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

Students from the Radboud University in Nijmegen that want to follow this course in the fall of 2015 should go to special information for Radboud University in Nijmegen

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 7, 2015 for the first part, and January 11, 2016 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 after every lecture):

date topic slides
Monday, November 9 Overview, pigeon hole formula, SAT is NP-complete, arithmetic in SAT 1 to 35
Thursday, November 12 Program correctness by SAT, resolution, Davis-Putnam, completeness 36 to 64
Monday, November 16 DPLL, conflict driven clause learning 65 to 94
Thursday, November 19 Tseitin transformation 95 to 108
Monday, November 23 Linear programming: Simplex method, SMT solving 109 to 138
Thursday, November 26 SMT solving, ILP is NP-hard, unique representation, reachability, NuSMV 139 to 167
Monday, November 30 NuSMV, Decision trees and BDDs 168 to 192
Thursday, December 3 BDDs 193 to 211
Monday, December 7 Predicate logic, resolution, unification 212 to 235
Thursday, December 10 Unification, resolution, Prolog 236 to 250
Monday, December 14 Prenex normal form, Skolemization, equational reasoning, term rewriting 250 to 268
Thursday, December 17 Term rewriting: main properties, termination undecidable, termination by monotone interpretations and lexicographic path order 268 to 285
Monday, January 4 Term rewriting: Newman's Lemma, critical pairs 286 to 298
Thursday, January 7 Term rewriting: word problem, Knuth-Bendix completion, overview course, old exam (last lecture) 299 to 311

Last change: November 23, 2015