date |
topic |
slides |
Monday, November 11 |
Overview, pigeon hole formula, SAT is NP-complete, arithmetic
in SAT |
1 to 36 |
Wednesday, November 13 |
Program correctness by SAT, resolution, Davis-Putnam, completeness |
37 to 65 |
Monday, November 18 |
DPLL, conflict driven clause learning |
66 to 87 |
Wednesday, November 20 |
Conflict driven clause learning, Tseitin transformation |
88 to 106 |
Monday, November 25 |
Linear programming: Simplex method |
107 to 135 |
Wednesday, November 27 |
SMT solving, unique representation, reachability, NuSMV |
136 to 161 |
Monday, December 2 |
NuSMV, Decision trees and BDDs |
162 to 185 |
Wednesday, December 4 |
BDDs |
186 to 206 |
Monday, December 9 |
Predicate logic, resolution, unification |
207 to 230 |
Wednesday, December 11 |
Unification, resolution, Prolog, prenex normal form |
231 to 248 |
Monday, December 16 |
Skolemization, equational reasoning, term rewriting |
248 to 263 |
Wednesday, December 18 |
Term rewriting: main properties, termination undecidable, termination by monotone
interpretations |
263 to 279 |
Monday, January 6 |
Term rewriting: lexicographic path order, Newman's Lemma, critical
pairs |
280 to 292 |
Wednesday, January 8 |
Term rewriting: word problem, Knuth-Bendix completion, overview course
(last lecture) |
293 to 306 |