### Content

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

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

06.03 & 09.03 | propositional logic, satisfiability, validity, conjunctive normal forms | pdf (x1, x4) | ||

13.03 & 16.03 | Horn formulas, SAT, Tseitin's transformation | pdf (x1, x4) | ||

20.03 & 23.03 | natural deduction, soundness | pdf (x1, x4) | ||

27.03 & 30.03 | completeness, resolution, binary decision diagrams | pdf (x1, x4) | ||

17.04 & 20.04 | binary decision diagrams, predicate logic (syntax) | pdf (x1, x4) | ||

24.04 & 27.04 | predicate logic (semantics), natural deduction | pdf (x1, x4) | ||

04.05 | ||||

08.05 & 11.05 | quantifier equivalences, unification, Skolemization | pdf (x1, x4) | ||

15.05 & 25.05 | resolution, undecidability, algebraic normal forms | pdf (x1, x4) | ||

22.05 & 01.06 | Post's adequacy theorem, CTL, CTL model-checking algorithm | pdf (x1, x4) | ||

05.06 & 15.06 | symbolic model checking, LTL | pdf (x1, x4) | ||

12.06 | adequacy, fairness, LTL model-checking algorithm | |||

19.06 & 22.06 | CTL*, SAT solving | |||

26.06 | 1st exam | |||

27.09 | 2nd exam | |||

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)