Content
The course provides an introduction to logic and model checking.Schedule
| date | topics | slides | exercises | solutions |
|---|---|---|---|---|
| 04.03 & 07.03 | propositional logic, satisfiability, validity, conjunctive normal forms | pdf (x1, x4) | ||
| 11.03 & 14.03 | Horn formulas, SAT, Tseitin's transformation | pdf (x1, x4) | ||
| 18.03 & 21.03 | natural deduction, soundness | pdf (x1, x4) | ||
| 08.04 & 11.04 | completeness, resolution, binary decision diagrams | pdf (x1, x4) | ||
| 15.04 & 18.04 | binary decision diagrams, predicate logic (syntax) | pdf (x1, x4) | ||
| 22.04 & 25.04 | predicate logic (semantics), natural deduction | pdf (x1, x4) | ||
| 29.04 & 02.05 | quantifier equivalences, unification, Skolemization | pdf (x1, x4) | ||
| 06.05 & 16.05 | resolution, undecidability, algebraic normal forms | pdf (x1, x4) | ||
| 13.05 & 23.05 | Post's adequacy theorem, CTL, CTL model-checking algorithm | pdf (x1, x4) | ||
| 27.05 & 06.06 | symbolic model checking, LTL | pdf (x1, x4) | ||
| 03.06 & 06.06 | adequacy, fairness, LTL model-checking algorithm | pdf (x1, x4) | ||
| 10.06 & 13.06 | CTL*, SAT solving, sorting networks | pdf (x1, x4) | ||
| 17.06 & 20.06 | SAT solving, sorting networks | pdf (x1, x4) | ||
| 24.06 | 1st exam (solution) | |||
| 20.09 | 2nd exam (solution) | |||
| 26.02 | 3rd exam |
Literature
The course is largely based on the following book:-
Michael Huth and Mark Ryan
Logic in Computer Science (second edition)
Cambridge University Press, 2007
ISBN 0-521-54310-X (paperback)