### Content

The course provides an introduction to logic and model checking.### Schedule

week | date | topics | slides | exercises | solutions |
---|---|---|---|---|---|

01 | 07.03 & 10.03 | propositional logic, satisfiability, validity, conjunctive normal forms | pdf (x1, x4) | ||

02 | 14.03 & 17.03 | Horn formulas, SAT, Tseitin's transformation | pdf (x1, x4) | ||

03 | 21.03 & 24.03 | natural deduction, soundness | pdf (x1, x4) | ||

04 | 28.03 & 31.03 | completeness, resolution, binary decision diagrams | pdf (x1, x4) | ||

05 | 04.04 & 07.04 | binary decision diagrams, predicate logic (syntax) | pdf (x1, x4) | ||

06 | 25.04 & 28.04 | predicate logic (semantics), natural deduction | pdf (x1, x4) | ||

07 | 02.05 & 05.05 | quantifier equivalences, unification, Skolemization | pdf (x1, x4) | ||

08 | 09.05 & 12.05 | resolution, undecidability, algebraic normal forms | pdf (x1, x4) | ||

09 | 16.05 & 19.05 | Post's adequacy theorem, CTL, CTL model-checking algorithm | pdf (x1, x4) | ||

10 | 23.05 & 02.06 | symbolic model checking, LTL | pdf (x1, x4) | ||

11 | 30.05 & 09.06 | adequacy, fairness, LTL model-checking algorithm | pdf (x1, x4) | ||

12 | 13.06 & 23.06 | CTL*, SAT solving, sorting networks | pdf (x1, x4) | ||

13 | 20.06 & 30.06 | sorting networks, SAT solving | pdf (x1, x4) | ||

27.06 | 1st exam (solution) | ||||

27.09 | 2nd exam (solution) | ||||

23.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)