date |
topic |
slides |
Monday, November 9 |
Overview, pigeon hole formula, SAT is NP-complete, arithmetic
in SAT |
1 to 35 |
Thursday, November 12 |
Program correctness by SAT, resolution, Davis-Putnam, completeness |
36 to 64 |
Monday, November 16 |
DPLL, conflict driven clause learning |
65 to 94 |
Thursday, November 19 |
Tseitin transformation |
95 to 108 |
Monday, November 23 |
Linear programming: Simplex method, SMT solving |
109 to 138 |
Thursday, November 26 |
SMT solving, ILP is NP-hard, unique representation, reachability, NuSMV |
139 to 167 |
Monday, November 30 |
NuSMV, Decision trees and BDDs |
168 to 192 |
Thursday, December 3 |
BDDs |
193 to 211 |
Monday, December 7 |
Predicate logic, resolution, unification |
212 to 235 |
Thursday, December 10 |
Unification, resolution, Prolog |
236 to 250 |
Monday, December 14 |
Prenex normal form, Skolemization, equational reasoning, term rewriting |
250 to 268 |
Thursday, December 17 |
Term rewriting: main properties, termination undecidable, termination by monotone
interpretations and lexicographic path order |
268 to 285 |
Monday, January 4 |
Term rewriting: Newman's Lemma, critical
pairs |
286 to 298 |
Thursday, January 7 |
Term rewriting: word problem, Knuth-Bendix completion, overview course, old exam
(last lecture) |
299 to 311 |