Search programme

​Use the search function to search amongst programmes at Chalmers. The study programme and the study programme syllabus relating to your studies are generally from the academic year you began your studies.

Syllabus for

Academic year
DAT060 - Logic in computer science
Logik för datavetenskap
 
Syllabus adopted 2021-02-26 by Head of Programme (or corresponding)
Owner: MPALG
7,5 Credits
Grading: TH - Pass with distinction (5), Pass with credit (4), Pass (3), Fail
Education cycle: Second-cycle
Major subject: Computer Science and Engineering, Software Engineering
Department: 37 - COMPUTER SCIENCE AND ENGINEERING


Teaching language: English
Application code: 02118
Open for exchange students: Yes
Block schedule: B

Module   Credit distribution   Examination dates
Sp1 Sp2 Sp3 Sp4 Summer course No Sp
0106 Examination 7,5c Grading: TH   7,5c   25 Oct 2021 am J,  03 Jan 2022 pm J,  15 Aug 2022 pm J

In programs

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

  Go to Course Homepage


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

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.


Page manager Published: Mon 28 Nov 2016.