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 |
139 to 163 |
Monday, November 30 |
NuSMV, Decision trees and BDDs |
164 to 194 |
Thursday, December 3 |
BDDs, predicate logic |
195 to 218 |
Monday, December 7 |
Predicate logic, resolution, unification |
219 to 240 |
Thursday, December 10 |
Unification, resolution, Prolog, prenex normal form, Skolemization |
241 to 258 |
Monday, December 14 |
Prover9, equational reasoning, term rewriting: main properties, termination undecidable |
259 to 278 |
Thursday, December 17 |
Termination by monotone interpretations and lexicographic path order, well-founded induction |
279 to 295 |
Monday, January 4 |
Term rewriting: Newman's Lemma, critical pairs, word problem, Knuth-Bendix completion |
296 to 317 |
Thursday, January 7 |
Critical pairs, overview course, old exam
(last lecture) |
318 |