Course syllabus

Jump to today

Course-PM

DAT060 / DIT203 Logic in Computer Science

LP1 HT26 (7.5 hp)

The course is offered by the department of Computer Science and Engineering.

News

Here we will publish news if there are any...

 

Contact Details

 

Course Purpose

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 solid 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. 

 

Schedule

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.
1.4.2
2 Natural deduction for propositional logic 1.1-1.3
3 Semantics of propositional logic, soundness and completeness, normal forms 1.4-1.5 except 1.4.2
4 Natural deduction and semantics for predicate logic 2.1-2.4
5

Undecidability of predicate logic and Post correspondence problem
Expressivity of predicate logic, compactness. SAT-solving.
Guest lecture on applications of propositional and predicate logic.

 2.5, 2.6
6

Expressivity of predicate logic, Gödel's incompleteness theorem and compactness.
Linear temporal logic, fixpoint.

 2.6, 3.1 and 3.2
7 LTL, CTL 3.2-3.5
8

Algorithms, fix-point characterization

Guest lecture on temporal logic.
Old exams

3.6-3.7


exam_231026.pdf

 

Exercises

Week 1: exercises1.pdf

Weeks 2--8: exercises2-8.pdf

Obs: We will go through different exercises in each of the exercise classes! So you should attend both of them.
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.

Non-obligatory Individual Assignments

There will be 6 non-obligatory individual assignments.
The assignments will not be graded, but in order to allow uploading files in canvas each assignment is given 1 point in canvas.

Solution to the assignments will be discussed in the Friday exercise session after the submission.

All submissions should be uploaded in Canvas. The solutions must be clear and readable; everything must be carefully motivated!

 

Course Literature

Logic in Computer Science by Michael Huth and Mark Ryan, second edition.
There is an electronic version at Store.
There is also an electronic version of the book available via Chalmers library.

Exercises marked with an asterisk ("*") in the text book have solutions.

 

Course Design

The course consists of a series of lectures, exercise sessions and non-obligatory weekly individual assignments.

The language of instruction is English.

 

Changes Made since the Last Occasion

This is a well-establish and working course and there are no changes on the content of the course compared to last year. On the other hand, bonus points were removed from the assignments given that it is very easy nowadays to get help from AI with their solutions. Assignment will still be available and students can get personalised feedback on their solutions.
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

Link to the syllabus on

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 are semantically valid,
  • explain the meaning of the soundness and completeness theorems for propositional and predicate calculus,
  • explain how to check if a linear-time and a branching-time temporal logic formula are valid in a given model.

Competence and skills:

  • write and check proofs in natural deduction for propositional and predicate calculus,
  • apply the soundness and completeness theorems to argue for the correctness of certain proofs,
  • argue semantically whether a given formula is the valid or not,
  • 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. 

 

Examination Form

The course is examined by an individual written exam taking place in an examination hall at the end of the course. 

Note:

When making a natural deduction proof in 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 nor in the exam unless their proof is also provided.

Exam

It is not allowed to have any help material but dictionaries to/from English during the written exams.

The exam has a maximum of 60 point. You must at least get 30 points in the exam in order to pass the course. The passing grades are as follows (both Chalmers and GU):

U 0-29
3 30-40
4 41-50
5 51-60

Exam Dates: 29th Oct 2026 am, 5th Jan 2027 am, 25th Aug 2026 am

Cheating

Any suspicious on cheating will be taken seriously and must be reported to the Disciplinary Committee for further investigation. 

 

Course Evaluation

Student Representatives

CTH

NN <nn @ student.chalmers.se>

GU

NN <nn @ student.gu.se>

Meetings

First meeting: TBA

Second meeting: TBA

Course summary:

Course Summary
Date Details Due