DAT060 / DIT203 Logic in Computer Science
LP1 HT23 (7.5 hp)
The course is offered by the department of Computer Science and Engineering.
Here we will publish news if there are any...
- Examiner and lecturer: Ana Bove <bove @ chalmers.se>
- Lecturer: Thierry Coquand <coquand @ chalmers.se>
- Teaching assistant:
- Freek Geerligs <geerligs @ chalmers.se>
- Hugo Moeneclaey <hugomo @ chalmers.se>
- Jeremy Pope <popje @ chalmers.se>
- Jonas Höfer <<hoferj @ chalmers.se>
Powerful tools for verifying software and hardware systems have been developed. These tools rely in a crucial way on logical techniques. This course provides a sound basis in logic and a short introduction to some logical frameworks used in modelling, specifying and verifying computer systems. A sound basic knowledge in logic is a welcome prerequisite for courses in program verification, formal methods and artificial intelligence.
See TimeEdit and/or course calendar.
Overview of Topics and Reading Material per Week
|Week||Topics||Reading Material/Book Sections|
|1||Motivation and organisation.
Recap logic, sets, relations, functions, induction
|sets relations functions notes on induction Structural induction
Note: There are 2 typos in the second page on set theory; the right most B in the distributive laws (1) and (2) should be an A.
|2||Natural deduction for propositional logic||1.1-1.3|
|3||Semantics of propositional logic, normal forms||1.4-1.5 except 1.4.2|
|4||Natural deduction and semantics for predicate logic||2.1-2.4|
Undecidability of predicate logic and Post correspondence problem
Expressivity of predicate logic, Gödel's incompleteness theorem and compactness.
|2.6, 3.1 and 3.2|
Guest lecture on temporal logic.
Repetition, old exams
Week 1: exercises1.pdf
Weeks 2--8: exercises2-8.pdf
Obs: We will go through different exercises in each of the exercise classes!
Part of Friday sessions will be used for discussing the solution to the assignment that was submitted the previous Tuesday.
Solutions: There are no solutions to the exercises other than those we link down here under course literature or from the calendar entry on specific exercise classes.
Logic in Computer Science by Michael Huth and Mark Ryan, second edition.
Exercises marked with an asterisk ("*") in the text book have solutions.
There is an electronic version of the book available via Chalmers library.
The course consists of a series of lectures and exercise sessions.
The language of instruction is English.
Changes Made since the Last Occasion
We will run the course fully on campus this year, besides this, no major changes from last year.
We will try to offer the two guest lectures that were offered last year (or similar ones) to better show the applications of the course, but this will depend on the availability of the teachers that could give these lectures.
Learning Objectives and Syllabus
After completing the course the student is expected to be able to:
Knowledge and understanding:
- explain when a given formula is a tautology,
- explain the notion of model of a first-order language and of temporal logic,
- explain when a first-order and a temporal logic formula is semantically valid,
- explain how to check if a branching-time temporal logic formula is valid in a given model,
- explain the meaning of the soundness and completeness theorems for propositional and predicate calculus.
Competence and skills:
- write and check proofs in natural deduction for propositional and predicate calculus,
- specify properties of a reactive system using linear-time temporal logic and branching time temporal logic.
Judgement and approach:
- judge the relevance of logical reasoning in computer science, i.e. for modelling computer systems,
- analyse the applicability of logical tools to solve problems in computer science, i.e. finding bugs with the use of model checking.
Link to the syllabus on
The course is examined by an individual written exam taking place in an examination hall at the end of the course. It is not allowed to have any help material but dictionaries to/from English.
The exams has a maximum of 60 points and the passing grades in the exam are as follow (both Chalmers and GU):
When making a natural deduction proof in the assignments (see below) and the exam you are allowed to use any of the rules presented in page 27 of the book plus the introduction and elimination rules for equality and for both the universal and existential quantifiers, unless it is stated otherwise in an exercise.
In other words, you are allowed to use all introduction and elimination rules (including those for double negation) and the derived rules MT, PBC and LEM, unless stated otherwise.
No other result can be used unless it is proved. This includes all provable equivalences stated in the slides of the lectures: they cannot be used in the assignments or the exams unless their proof is also provided.
There will be 6 non-obligatory individual assignments with a total of 60 to 65 points. The first five assignment have 10 points and the last one has 10 to 15 points. 10% of the total number of points obtained with the assignments count as bonus points in the written exam. These bonus points are valid for the whole academic year 23/24.
Solution to the assignments will be discussed in the Friday exercise session after the submission.
All submissions must include name, and personal number and should be uploaded in Canvas. The solutions must be clear and readable; everything must be carefully motivated!
As always in life, one should not cheat! Any suspicious on cheating will be taken seriously and must be reported to the Disciplinary Committee for further investigation.
Exam dates for 2023/2024: 26th Oct 2023, 3rd Jan 2024, 28th Aug 2024
Adithya Bijoy <adithya1210571 @ gmail.com>
Armaan Rashid <armaan @ student.chalmers.se>
Nor Führ <pingu @ student.chalmers.se>
Nazif Kadiroglu <nazif @ student.chalmers.se>
Samuel Kyletoft <kyletoft @ student.chalmers.se>
Elin Melander <gusmelelb @ student.gu.se>
Josefin Kokkinakis <guskokkijo @ student.gu.se>
Moa Ahlberg <gusahlbmo @ student.gu.se>
William Kangas <guskangwi @ student.gu.se>
First meeting: Thursday 14th of September 15:15. Protocol.
Second meeting: Thursday 12th of October 9:00. Protocol.
The syllabus page shows a table-oriented view of course schedule and basics of course grading. You can add any other comments, notes or thoughts you have about the course structure, course policies or anything else.
To add some comments, click the 'Edit' link at the top.