Content
The course provides an introduction to logic and model checking.Schedule
| date | topics | slides | exercises | solutions |
|---|---|---|---|---|
| 02.03 & 05.03 & 12.03 | propositional logic, satisfiability, validity, conjunctive normal forms | |||
| 09.03 & 19.03 | Horn formulas, SAT, Tseitin's transformation | |||
| 16.03 & 26.03 | natural deduction, soundness | |||
| 23.03 & 16.04 | completeness, resolution, binary decision diagrams | |||
| 13.04 & 23.04 | binary decision diagrams, predicate logic (syntax) | |||
| 20.04 & 30.04 | predicate logic (semantics), natural deduction | |||
| 27.04 & 07.05 | quantifier equivalences, unification, Skolemization | |||
| 04.05 & 21.05 | resolution, undecidability, algebraic normal forms | |||
| 11.05 & 21.05 | Post's adequacy theorem, CTL, CTL model-checking algorithm | |||
| 18.05 & 28.05 | symbolic model checking, LTL | |||
| 01.06 & 11.06 | adequacy, fairness, LTL model-checking algorithm | |||
| 08.06 & 18.06 | CTL*, SAT solving, sorting networks | |||
| 15.06 & 25.06 | SAT solving, sorting networks | |||
| 22.06 | compactness, second-order logic, first-order theories | |||
| 29.06 | 1st exam | |||
| ??.09 | 2nd exam | |||
| ??.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)