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 223 |
Monday, December 12 |
Predicate logic, resolution, unification |
224 to 246 |
Thursday, December 15 |
Unification, resolution, Prolog, prenex normal form, Skolemization, Prover9 |
247 to 262 |
Monday, December 19 |
Equational reasoning, term rewriting: main properties, termination undecidable |
263 to 278 |
Thursday, December 22 |
Termination by monotone interpretations and lexicographic path order, well-founded induction, Newman's Lemma |
279 to 297 |
Monday, January 9 |
Term rewriting: critical pairs, word problem, Knuth-Bendix completion |
298 to 315 |
Thursday, January 12 |
Critical pairs, overview course, old exam
(last lecture) |
316 to 318 |