Content

The course provides an introduction to logic and model checking.

Schedule

date	topics	slides	exercises	solutions
03.03 & 06.03 & 13.03	propositional logic, satisfiability, validity, conjunctive normal forms	pdf (x1, x4)	pdf
10.03 & 20.03	Horn formulas, SAT, Tseitin's transformation	pdf (x1, x4)	pdf
17.03 & 27.03	natural deduction, soundness	pdf (x1, x4)	pdf
24.03 & 03.04	completeness, resolution, binary decision diagrams
31.03 & 10.04	binary decision diagrams, predicate logic (syntax)
07.04 & 08.05	predicate logic (semantics), natural deduction
28.04 & 08.05	quantifier equivalences, unification, Skolemization
05.05 & 15.05	resolution, undecidability, algebraic normal forms
12.05 & 22.05	Post's adequacy theorem, CTL, CTL model-checking algorithm
19.05 & 05.06	symbolic model checking, LTL
26.05 & 12.06	adequacy, fairness, LTL model-checking algorithm
02.06 & 12.06	CTL*, SAT solving, sorting networks
16.06	SAT solving, sorting networks
23.06	1st exam
25.09	2nd exam
26.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)

Slides as well as solutions to selected exercises will be made available online.