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
13.03 & 16.03	Horn formulas, SAT, Tseitin's transformation
20.03 & 23.03	natural deduction, soundness
27.03 & 30.03	completeness, resolution, binary decision diagrams
17.04 & 20.04	binary decision diagrams, predicate logic (syntax)
24.04 & 27.04	predicate logic (semantics), natural deduction
24.04 & 04.05
08.05 & 11.05	quantifier equivalences, unification, Skolemization
15.05 & 25.05	resolution, undecidability, algebraic normal forms
22.05 & 01.06	Post's adequacy theorem, CTL, CTL model-checking algorithm
05.06 & 15.06	symbolic model checking, LTL
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)

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