date |
topic |
slides |
Monday, November 14 |
Overview, pigeon hole formula, SAT is NP-complete, arithmetic (addition)
in SAT |
1 to 33 |
Thursday, November 17 |
Multiplication, program correctness by SAT, resolution, Davis-Putnam procedure |
33 to 59 |
Monday, November 21 |
Completeness of resolution, DPLL, conflict driven clause learning |
60 to 86 |
Thursday, November 24 |
Conflict driven clause learning, Tseitin transformation |
87 to 109 |
Monday, November 28 |
Linear programming: Simplex method, SMT solving |
110 to 141 |
Thursday, December 1 |
SMT solving, ILP is NP-hard, unique representation, reachability |
142 to 165 |
Monday, December 5 |
NuSMV, Decision trees and BDDs |
166 to 194 |
Thursday, December 8 |
BDDs, predicate logic |
195 to 218 |
Monday, December 12 |
Predicate logic, resolution, unification |
219 to 240 |
Thursday, December 15 |
Unification, resolution, Prolog, prenex normal form, Skolemization |
241 to 258 |
Monday, December 19 |
Prover9, equational reasoning, term rewriting: main properties, termination undecidable |
259 to 278 |
Thursday, December 22 |
Termination by monotone interpretations and lexicographic path order, well-founded induction |
279 to 295 |
Monday, January 9 |
Term rewriting: Newman's Lemma, critical pairs, word problem, Knuth-Bendix completion |
296 to 317 |
Thursday, January 12 |
Critical pairs, overview course, old exam
(last lecture) |
318 |