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 |