Information about the course Automated Reasoning (2IMF25)

This course will be given in the fall of 2018, in the second quartile.
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.
Lectures from 2013 (having code 2IW15) are available on video

Teacher: Prof Dr H. Zantema, Metaforum 6.078, tel 2749, h.zantema@tue.nl

Students from the Radboud University in Nijmegen that (want to) follow this course should go to special information for Radboud University

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 13, 2018 for the first part, and January 10, 2019 for the second part.
The reports of the practical assignment should be handed in via Canvas.


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
Monday, November 12 Overview, pigeon hole formula, SAT is NP-complete, arithmetic (addition) in SAT 1 to 33
Thursday, November 15 Multiplication, program correctness by SAT, resolution, Davis-Putnam procedure 34 to 59
Monday, November 19 Completeness of resolution, DPLL, conflict driven clause learning 60 to 91
Thursday, November 22 Dimacs format, Tseitin transformation, 8 queens, rectangle fitting 92 to 110, MOOC examples 30-60
Monday, November 26 Linear programming: Simplex method, SMT solving 111 to 145
Thursday, November 29 SMT solving, examples, ILP is NP-complete, unique representation 146 to 162
Monday, December 3 Reachability, NuSMV, Decision trees 163 to 187
Thursday, December 6 BDDs 188 to 207
Monday, December 10 BDDs, Predicate logic, resolution, unification 208 to 239
Thursday, December 13 Unification, Prolog, prenex normal form, Skolemization, Prover9, equational reasoning 240 to 270
Monday, December 17 Term rewriting: main properties, termination undecidable, termination by monotone interpretations 271 to 288
Thursday, December 20 Termination by monotone interpretations and lexicographic path order, well-founded induction, Newman's Lemma, critical pairs 289 to 304
Monday, January 7 Term rewriting: critical pairs, word problem, Knuth-Bendix completion 305 to 315
Thursday, January 10 Critical pairs, overview course, old exam (last lecture) 316 to 321



Last change: December 10, 2018