date |
topic |
slides |
Monday, November 13 |
Overview, pigeon hole formula, SAT is NP-complete, arithmetic (addition)
in SAT |
1 to 33 |
Thursday, November 16 |
Multiplication, program correctness by SAT, resolution, Davis-Putnam procedure |
33 to 59 |
Monday, November 20 |
Completeness of resolution, DPLL, conflict driven clause learning |
60 to 86 |
Thursday, November 23 |
Conflict driven clause learning, Tseitin transformation |
87 to 109 |
Monday, November 27 |
Linear programming: Simplex method, SMT solving |
110 to 141 |
Thursday, November 30 |
SMT solving, ILP is NP-hard, unique representation, reachability |
142 to 165 |
Monday, December 4 |
NuSMV, Decision trees and BDDs |
166 to 194 |
Thursday, December 7 |
BDDs, predicate logic |
195 to 223 |
Monday, December 11 |
Predicate logic, resolution, unification |
224 to 246 |
Thursday, December 14 |
Unification, resolution, Prolog, prenex normal form, Skolemization, Prover9 |
247 to 262 |
Monday, December 18 |
Equational reasoning, term rewriting: main properties, termination undecidable |
263 to 278 |
Thursday, December 21 |
Termination by monotone interpretations and lexicographic path order, well-founded induction, Newman's Lemma |
279 to 297 |
Monday, January 8 |
Term rewriting: critical pairs, word problem, Knuth-Bendix completion |
298 to 315 |
Thursday, January 11 |
Critical pairs, overview course, old exam
(last lecture) |
316 to 318 |