Content
The course provides an introduction to logic and model checking.Schedule
| lecture | date | topics |
|---|---|---|
| 1 | 01.10 & 04.10 | propositional logic, satisfiability, validity, conjunctive normal forms |
| 2 | 08.10 & 11.10 | Horn formulas, SAT, Tseitin's transformation |
| 3 | 15.10 & 18.10 | natural deduction, soundness |
| 4 | 22.10 & 25.10 | completeness, resolution, binary decision diagrams |
| 5 | 29.10 |
binary decision diagrams, algebraic normal forms, functional completeness |
| 6 | 05.11 & 08.11 | Post's adequacy theorem, SAT solving, sorting networks |
| 7 | 12.11 & 15.11 | sorting networks, SAT solving |
| 8 | 19.11 & 22.11 | linear-time temporal logic, adequacy |
| 9 | 26.11 & 29.11 | branching-time temporal logic, adequacy, CTL model-checking algorithm |
| 10 | 03.12 & 06.12 | fairness, CTL*, symbolic model checking |
| 11 | 10.12 & 13.12 | predicate logic (syntax and semantics), natural deduction |
| 12 | 07.01 & 10.01 | natural deduction, quantifier equivalences, unification |
| 13 | 14.01 & 17.01 | Skolemization, resolution, undecidability |
| 14 | 21.01 & 24.01 | first-order theories, Gödel's incompleteness theorem, SMT |
| 15 | 28.01 | 1st 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)