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 192 |
Wednesday, December 3 |
BDDs |
193 to 211 |
Monday, December 8 |
Predicate logic, resolution, unification |
212 to 235 |
Wednesday, December 10 |
Unification, resolution, Prolog |
236 to 250 |
Monday, December 15 |
Prenex normal form, Skolemization, equational reasoning, term rewriting |
250 to 268 |
Wednesday, December 17 |
Term rewriting: main properties, termination undecidable, termination by monotone
interpretations and lexicographic path order |
268 to 285 |
Monday, January 5 |
Term rewriting: Newman's Lemma, critical
pairs |
286 to 297 |
Wednesday, January 7 |
Term rewriting: word problem, Knuth-Bendix completion, overview course
(last lecture) |
298 to 311 |