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)