Course syllabus adopted 2021-02-26 by Head of Programme (or corresponding).
Overview
- Swedish nameLogik för datavetenskap
- CodeDAT060
- Credits7.5 Credits
- OwnerMPALG
- Education cycleSecond-cycle
- Main field of studyComputer Science and Engineering, Software Engineering
- DepartmentCOMPUTER SCIENCE AND ENGINEERING
- GradingTH - Pass with distinction (5), Pass with credit (4), Pass (3), Fail
Course round 1
- Teaching language English
- Application code 02136
- Block schedule
- Open for exchange studentsYes
Credit distribution
Module | Sp1 | Sp2 | Sp3 | Sp4 | Summer | Not Sp | Examination dates |
|---|---|---|---|---|---|---|---|
| 0106 Examination 7.5 c Grading: TH | 7.5 c |
|
In programmes
- MPALG - COMPUTER SCIENCE - ALGORITHMS, LANGUAGES AND LOGIC, MSC PROGR, Year 1 (compulsory)
- MPCSN - COMPUTER SYSTEMS AND NETWORKS, MSC PROGR, Year 2 (elective)
Examiner
Ana Bove- Head of Unit, Computing Science, Computer Science and Engineering
Eligibility
General entry requirements for Master's level (second cycle)Applicants enrolled in a programme at Chalmers where the course is included in the study programme are exempted from fulfilling the requirements above.
Specific entry requirements
English 6 (or by other approved means with the equivalent proficiency level)Applicants enrolled in a programme at Chalmers where the course is included in the study programme are exempted from fulfilling the requirements above.
Course specific prerequisites
The requirement for the course is to have successfully completed two years with the subject Computer Science or equivalent. Particularly relevant are Mathematics (including Discrete mathematics), Programming, Algorithms and/or data structures.Aim
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.Learning outcomes (after completion of the course the student should be able to)
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
- 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
- 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
Content
The course covers propositional and predicate calculus, and model-checking. More concretely, the course gives a thorough introduction to fundamental notions of logic such as natural deduction, semantics of both propositional and predicate calculus, soundness and completeness, conjunctive normal forms, Horn clauses, undecidability and expressiveness of predicate logic, plus an introduction to model checking: Linear-time temporal logic (LTL) and Branching-time temporal logic (CTL).Organisation
The course consists of lectures, exercise sessions and non-obligatory assignments.Literature
Huth, Ryan. Logic in Computer Science, see http://www.cs.bham.ac.uk/research/lics/Examination including compulsory elements
The course is examined by an individual written exam at the end of the course taking place in an examination hall.Non-obligatory individual assignments which grant bonus points for the written exam are offered during the course. The bonus points are valid through the whole academic year.
The course examiner may assess individual students in other ways than what is stated above if there are special reasons for doing so, for example if a student has a decision from Chalmers on educational support due to disability.