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 185 |
Wednesday, December 3 |
BDDs |
186 to 206 |
Monday, December 8 |
Predicate logic, resolution, unification |
207 to 230 |
Wednesday, December 10 |
Unification, resolution, Prolog, prenex normal form |
231 to 248 |
Monday, December 15 |
Skolemization, equational reasoning, term rewriting |
248 to 263 |
Wednesday, December 17 |
Term rewriting: main properties, termination undecidable, termination by monotone
interpretations |
263 to 279 |
Monday, January 5 |
Term rewriting: lexicographic path order, Newman's Lemma, critical
pairs |
280 to 292 |
Wednesday, January 7 |
Term rewriting: word problem, Knuth-Bendix completion, overview course
(last lecture) |
293 to 306 |