Course syllabus
Course-PM
DAT060 / DIT201 Logic in Computer Science
LP1 HT19 (7.5 hp)
The course is offered by the department of Computer Science and Engineering.
Contact Details
- Examiner and lecturer: Thierry Coquand <coquand @ chalmers.se>
- Lecturer: Ana Bove <bove @ chalmers.se>
- Teaching assistant:
- Fabian Ruch <fabian.ruch @ cse.gu.se>
- Nachiappan Valliappan <nacval @ chalmers.se>
Course Purpose
In recent years, powerful tools for verifying software and hardware systems have been developed. These tools rely in a crucial way in 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.
Schedule
Overview of Topics and Reading Material per Week
| Week | Topics | Reading Material/Book Sections |
| 1 | Recap logic, sets, relations, functions, induction |
sets relations functions notes on induction Structural induction 1.4.2 |
| 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 |
| 5 | Undecidability of predicate logic | 2.5 |
| 6 |
Expressivity of predicate logic, compactness. Guest lecture. |
2.6 |
| 7 | LTL, CTL | 3.2-3.5 |
| 8 |
Algorithms, fix-point characterization Repetition, old exams |
3.6-3.7 |
Course Literature
Logic in Computer Science by Michael Huth and Mark Ryan, second edition.
See http://www.cs.bham.ac.uk/research/lics/
Exercises marked with an asterisk ("*") in the text book have solutions.
There is an electronic version of the book available via Chalmers library.
Course Design
The course consists of a series of lectures and exercise sessions.
The language of instruction is English.
Changes Made since the Last Occasion
- Added two extra lectures with recap on sets, relations, functions and induction.
- Added and extra exercise/consultation session to discuss the solution to assignments and provide possibility to ask questions to the assistants.
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 the meaning of the completeness and soundness theorems;
- explain the notion of model for temporal logic, when a temporal formula is semantically valid and how to check if a branching-time temporal logic formula is valid in a given model;
- describe the content 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
- Chalmers Studieportalen Study plan
- Göteborgs Universitet Course plan
Examination Form
The course is examined by an individual written exam taken place in an examination hall at the end of the course.
No help is allowed during the written exam except for English dictionaries.
The exams has a maximum of 60 points and the passing grades in the exam are as follow:
| Chalmers | |
| GU |
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 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.
Non-obligatory assignments:
There will be 5-6 non-obligatory individual assignments. Each assignment gives up to ten points and 10% of those points count as bonus points in the written exam. These bonus points are valid for the whole academic year 19/20.
The first deadline is in study week three, i.e. Thursday September 19th at 15:00. You can hand them in the return box by the printers and restrooms on the 6th floor (between computer room ES61 and group room EG-6207) or to the teacher at the lecture. Please do not hand them in by email.
Solution to the assignments will be discussed in the Friday exercise session after the submission.
Graded submissions will be handed back during one of the exercise session one week after the submission.
All submissions must include your name, personal number and email address, and be stapled together. Your solutions must be clear and readable; everything must be carefully motivated!
As always in life, you 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 2019/2020: 29th of October 2019 pm, 7th of January 2020 pm, 17th of August 202 pm.
Course Evaluation
Student Representatives
CTH
- Adi Hrustic (hrustic @ student.chalmers.se)
- Jie Song (song @ student.chalmers.se)
- Oskar Vigren (vioskar @ student.chalmers.se)
- Karl Wikström (karlwik @ student.chalmers.se)
- Samuel Rörgren (rorgren @ student.chalmsers.se)
GU
- David Hultsten (gushultsda @ student.gu.se)
- Juliana Siburian (gussibju @ student.gu.se)
Meetings
First meeting: Thursday 19/9 15:15. Protocol.
Second meeting: Thursday 17/10 15:15. Protocol.
Course summary:
| Date | Details | Due |
|---|---|---|