18 Aug: A test exam and a past exam with solutions
The goal of the course is to present the fundamental basic notions of logic that are important in computer science. One presents propositional and predicate logic in natural deductions the way it is done in most interactive theorem provers, with a suggestive box notations for proofs. One presents also the basis of model checking and temporal logic (LTL and CTL). One does not cover a detailed proof of completeness theorem for predicate logic (and one gives a sktech of completeness for propositional logic) but what is important is that the students understand well the -meaning- of the various completeness theorems. (On the other hand one gives a proof of undecidability of predicate logic via Post systems.) In the same spirit, one does not present complete proofs of decidability for LTL and CTL but one presents in detail the fixed-point semantics of CTL.
The content of the course is roughly the 3 first chapters of Huth and Ryan "Logic in Computer Science".
There are some slides motivating the course.
This course use Logic in Computer Science by Michael Huth and Mark Ryan.
| Week | Tuesday | Wednesday | Chapters | Topics | Exercises |
|---|---|---|---|---|---|
| 1 | 30 Aug | 31 Aug | 1.1, 1.2 | Propositional logic, natural deduction | Week 1 |
| 2 | 6 sep | 7 sep | 1.3, 1.4, 1.5 | formal language, proof by induction, semantics, normal form | Week 2 |
| 3 | 13 sep | 14 sep | 2.1, 2.2 | Predicate logic as a formal language | Week 3 |
| 4 | 20 sep | 21 sep | 2.3,2.4 | Semantics of predicate logic | Week 4 |
| 5 | 27 sep | 28 sep | 2.5, 2.6, 3.1, 3.2 | Undecidability, expressivity of predicate logic; Model checking | Week 5 |
| 6 | 4 oct | 5 oct | 3.3, 3.4, 3.5, 3.6 | LTL, CTL | Week 6 |
| 7 | 11 oct | 12 oct | 3.7 | Algorithms, fixed-point characterisation, repetition | Week 7 |
No books or written help during the exam.
Here is a list of exercices from a previous year, some with comments. Since time is short there are no guarentees that all exercises will be covered during the exercise session on Fridays. Exercises marked with a * in the text book have solutions.
An interactive introduction to natural deduction for propositional and predicate calculus with several good examples.
A text on the tree method (looking systematically for a countermodel)
The chapter 7 of the book Artificial Intelligence: A Modern Approach contains a brilliant introduction to propositional logic, complementary to the one of the book of Huth and Ryan.
A prover to practise natural deduction (only for propositional logic).
A short note on how to decide an LTL formula. This is not required for the exam, but I found the explanations in the book difficult to follow and wanted to have a method which can be applied by hand on small examples.
A general presentation of some notions of the course and a nice application of the use of temporal logic.
Feel free to contact Jan Smith, Thierry Coquand or/and Simon Huber in case you have any questions or problems. Almost everything you get in the class is available electronically. Send me a request if you have missed some stuff.