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 6.078, tel 2749, 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: 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 10 Overview, pigeon hole formula, SAT is NP-complete, arithmetic in SAT 1 to 36
Wednesday, November 12 Program correctness by SAT, resolution, Davis-Putnam, completeness 37 to 64
Monday, November 17 DPLL, conflict driven clause learning 65 to 89
Wednesday, November 19 Conflict driven clause learning, Tseitin transformation 90 to 110
Monday, November 24 Linear programming: Simplex method, SMT solving 111 to 140
Wednesday, November 26 SMT solving, ILP is NP-hard, unique representation, reachability, NuSMV 141 to 167
Monday, December 1 NuSMV, Decision trees and BDDs 168 to 192
Wednesday, December 3 BDDs 193 to 211
Monday, December 8 Predicate logic, resolution, unification 212 to 235
Wednesday, December 10 Unification, resolution, Prolog 236 to 250
Monday, December 15 Prenex normal form, Skolemization, equational reasoning, term rewriting 250 to 268
Wednesday, December 17 Term rewriting: main properties, termination undecidable, termination by monotone interpretations and lexicographic path order 268 to 285
Monday, January 5 Term rewriting: Newman's Lemma, critical pairs 286 to 297
Wednesday, January 7 Term rewriting: word problem, Knuth-Bendix completion, overview course (last lecture) 298 to 311



Last change: December 17, 2014