### 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)