2012-11-12: The exam review is on Thursday, November 15, 15:00-15:45 in room 6128.
2012-10-25: Suggested solutions for the exam can be found here.
2012-10-22: On tuesday (2012-10-23) you can pick up the corrected assignment 6 in room 6103 in the EDIT building between 15:00-16:00.
2012-10-22: On behalf of our two rectors, I'm doing an investigation of how to increase the cooperation between GU and Chalmers, both concerning research and education. Since this course is joint between Chalmers and GU, I'm very intrested in views on how it works with a joint course, e.g. are there any problem you can tell me about. Please, send me a mail if you have an opinion on this! Jan.
2012-10-20: Yet another exam from last year.
2012-10-19: A list of topics especially relevant for the exam.
2012-10-16: Here is another exam from last year.
2012-10-11: Assignment 6 is now on the webpage.
2012-10-04: Here is an old test exam and a past exam with solutions.
2012-10-03: Assignment 5 is now on the webpage.
2012-10-01: Note that we assume that = binds stronger than forall in Assignment 4. This means that \forall x f(f(x)) = f(x) should be interpreted as \forall x (f(f(x)) = f(x)).
2012-09-27: Here is the list of (randomly selected) Student Representatives.
2012-09-27: Assignment 4 is now on the webpage.
2012-09-20: Assignment 3 is now on the webpage.
2012-09-14: Added a clarification to the information on assignments that computer written solutions must be handed in as either a pdf or txt file.
2012-09-13: If you are writing your solutions to the assignments using LaTeX and want your proofs to look like those in the book you can use the Proof boxes package.
2012-09-12: Assignment 2 is now on the webpage.
GU-students have to register in the Student Portal (see below).
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 notation 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 sketch 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 uses Logic in Computer Science by Michael Huth and Mark Ryan.
This semester GU-students have to register online in LPW at the Student Portal. The registration is obligatory in order to attend the course. Note that you need to register yourself on the course the same day as the first lecture, otherwise you will lose your place. For further information about the registration and how to activate your student account see here.
| Week | Chapters | Topics | Exercises | Assignments |
|---|---|---|---|---|
| 1 | 1.1, 1.2 | Propositional logic, natural deduction | Week 1 | |
| 2 | 1.3, 1.4, 1.5 | Formal language, proof by induction, semantics, normal form | Week 2 | |
| 3 | 2.1, 2.2, 2.3 | Predicate logic, natural deduction | Week 3 | |
| 4 | 2.4 | Semantics of predicate logic | Week 4 | |
| 5 | 2.5, 2.6 | Undecidability, expressivity of predicate logic | Week 5 | |
| 6 | 3.2, 3.3, 3.4, 3.5 | LTL, CTL | Week 6 | |
| 7 | 3.6, 3.7 | Algorithms, fixed-point characterisation, repetition | Week 7 | - |
The exam has 60 points in total. No books or written help during the exam.
There will be six non-obligatory assignments which should be handed in individually. Each assignment gives ten points and 10% of those points count as bonus points in the exam. The bonus points are only valid for the exams held before February 2013.
Your solutions must be handed in before the weekly exercise session. The first deadline is in study week two, i.e., September 14th, 10:00. You can hand them in either by email to Anders, in the lectures, in the beginning of the exercise session, or in office 6103A.
All submissions must include your name, email address, and be stapled together. If you want to send your answers by email, the solution must be either a pdf file or txt file (where pdf is preferred). Your solutions must be clear and readable; everything must be carefully motivated!
As always in life, you should not cheat! Cheating will be taken seriously and will be reported to the Disciplinary Commitee for further investigation.
Here is a list of exercises from a previous year, some with comments. 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)
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.
jan(dot)smith(at)chalmers(dot)se
Simon Huber,
mail: simonhu(at)chalmers(dot)se
mortberg(at)chalmers(dot)se