Information about the course Automated Reasoning (2IW15)

This course has been given in the fall of 2011, on Monday from 8.45 to 10.30. The last lecture was on December 19; in January there are no more lectures.
Lectures from 2009 are available on video

Teacher: Prof Dr H. Zantema, HG 6.73, 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:

• Satisfiability of propositions: tableaux method, resolution, and the main ingredients of modern satisfiability provers.
  
• Satisfiability modulo theories.
  
• Binary Decision Diagrams as efficient representation of boolean expressions.
  
• Unification; resolution on predicates.
  
• Reasoning modulo equations, term rewriting.

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: November 14, 2011 for the first part, and January 9, 2012 for the second part. To improve your result from January 2012 you may do an extra set of problems to be downloaded below, deadline April 2, 2012

For both parts, the written exam and the practical assignment, the grade should be at least 5. 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:

• The slides used in the course in handout format, version September 1, 2011.
  
• For the practical assignment:
  
  
  
  • The text for the assignment in PDF format, including guidelines and the problems to be solved.
  • The text for the set of extra problems in PDF format, to improve the results of the practical assignment of January 2012. The deadline for this additional assignment is April 2, 2012.
  • An example of how to present the solution of a problem for the practical assignment. Also the LaTeX source of this example is available.
    
  • The tool yices: a program for satisfiability modulo theories (smt). It accepts smt format, but can also be used as a boolean SAT solver accepting dimacs format.
  • The tool bddsolve: a program based on BDDs. It can be used for satisfiability and counting the number satisfying assignments, and for reachability.
  
  
• Some old exams.
  
  • November, 2006, with solutions
    
  • June, 2009
    
  • August, 2009
    
  • June, 2010
    
  • August, 2010
    
  • June, 2011, with solutions
    
  • August, 2011
    
  • January, 2012

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


Lectures and topics:

date	topic	slides
September 5	Overview, pigeon hole formula, SAT is NP-complete, arithmetic in SAT	1 to 31
September 12	Arithmetic and program correctness in prop.logic, semantic tableaux	32 to 46
September 19	Resolution: DP, completeness, DPLL	47 to 74
September 26	DPLL, proof system, optimizations: backjump, learn, forget, restart	75 to 97
October 3	Tseitin transformation, extension of SAT: SMT	98 to 121
October 10	Pseudo boolean constraints, unique representation, reachability, decision trees, BDDs	122 to 151
October 17	Reduced ordered BDDs: definition and algorithms	152 to 166
October 24	BDD application: hardware verification and pseudo boolean constraints. Predicates: semantic tableaux	167 to 191
November 14	Predicates: resolution, unification	192 to 210
November 21	Resolution, Prolog, SLD resolution, prenex normal form	211 to 224
November 28	Skolemization. Term rewriting: definition, weak and strong normalisation	225 to 237
December 5	Confluence, undecidability of termination, termination by monotonic interpretations	238 to 252
December 12	Termination by lexicographic path order, Newman's Lemma, analyzing WCR by critical pairs	253 to 266
December 19	Word problem for complete TRSs, Knuth Bendix completion, course overview	267 to 281

Last change: February 8, 2012