Content
The course provides an introduction to logic and model checking. The following topics are discussed:- propositional logic: syntax, semantics, natural deduction, soundness and completeness, conjunctive normal forms, Horn clauses, SAT solvers, resolution, binary decision diagrams, Post's adequacy theorem
- predicate logic: syntax, semantics, natural deduction, undecidability, first-order theories, compactness, expressiveness, unification, resolution, Skolemization
- model checking: linear-time temporal logic, branching-time temporal logic, algorithms, fixed-point characterisation, symbolic model checking
Schedule
| week | date | slides | exercises | solutions | material |
|---|---|---|---|---|---|
| 1 | 03.10 & 06.10 & 11.10 | pdf (4x1) | link | ||
| 2 | 10.10 & 13.10 & 18.10 | pdf (4x1) | |||
| 3 | 17.10 & 20.10 & 25.10 | pdf (4x1) | |||
| 4 | 24.10 & 27.10 & 08.11 | pdf (4x1) | link | ||
| 5 | 31.10 & 03.11 & 08.11 | pdf (4x1) | |||
| 6 | 07.11 & 10.11 & 15.11 | pdf (4x1) | |||
| 7 | 14.11 & 17.11 & 22.11 | pdf (4x1) | |||
| 8 | 21.11 & 24.11 & 29.11 | pdf (4x1) | |||
| 9 | 28.11 & 01.12 & 06.12 | pdf (4x1) | |||
| 10 | 05.12 |
pdf (4x1) | |||
| 11 | 12.12 & 15.12 & 10.01 | pdf (4x1) | link | ||
| 12 | 09.01 & 12.01 & 17.01 | pdf (4x1) | |||
| 13 | 16.01 & 19.01 & 24.01 | pdf (4x1) | link | ||
| 14 | 23.01 & 26.01 & 31.01 | pdf (4x1) | |||
| 15 | 30.01 & 02.02 (exam) | pdf (4x1) |
Literature
The course is largely based on the following book:-
Michael Huth and Mark Ryan
Logic in Computer Science (second edition)
Cambridge University Press, 2004
ISBN 0-521-54310-X (paperback)