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 solving, resolution, binary decision diagrams, Post's adequacy theorem, sorting networks
- predicate logic: syntax, semantics, natural deduction, undecidability, first-order theories, Gödel's incompleteness theorem, 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 | 02.10 & 05.10 | ||||
| 2 | 09.10 & 12.10 | ||||
| 3 | 16.10 & 19.10 | ||||
| 4 | 23.10 |
||||
| 5 | 30.10 |
||||
| 6 | 06.11 & 09.11 | ||||
| 7 | 13.11 & 16.11 | ||||
| 8 | 20.11 & 23.11 | ||||
| 9 | 27.11 & 30.11 | ||||
| 10 | 04.12 & 07.12 | ||||
| 11 | 11.12 & 14.12 | ||||
| 12 | 08.01 & 11.01 | ||||
| 13 | 15.01 & 18.01 | ||||
| 14 | 22.01 & 25.01 | ||||
| 15 | 29.01 & 01.02 | exam (practice) |
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)