Content
The course provides an introduction to logic and model checking.Schedule
| lecture | date | topics | slides | solutions | material |
|---|---|---|---|---|---|
| 1 | 02.03 & 05.03 | propositional logic, satisfiability, validity, conjunctive normal forms | |||
| 2 | 09.03 & 12.03 | Horn formulas, SAT, Tseitin's transformation | |||
| 3 | 16.03 & 19.03 | natural deduction, soundness | |||
| 4 | 23.03 & 26.03 | completeness, resolution, binary decision diagrams | |||
| 5 | 30.03 & 02.04 | binary decision diagrams, algebraic normal forms, functional completeness | |||
| 6 | 20.04 & 23.04 | Post's adequacy theorem, SAT solving, sorting networks | |||
| 7 | 27.04 & 30.04 | sorting networks, SAT solving | |||
| 8 | 04.05 & 07.05 | linear-time temporal logic, adequacy | |||
| 9 | 11.05 & 14.05 | branching-time temporal logic, CTL model-checking algorithm, adequacy | |||
| 10 | 18.05 & 28.05 | fairness, CTL*, symbolic model checking | |||
| 11 | 25.05 & 04.06 | predicate logic (syntax and semantics), natural deduction | |||
| 12 | 08.06 | natural deduction, quantifier equivalences, unification | |||
| 13 | 15.06 & 18.06 | Skolemization, resolution, undecidability | |||
| 14 | 22.06 | 1st exam | |||
| 25.09 | 2nd exam | ||||
| 25.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)