Logic in Computer Science

The course can be part of the following programmes:

1. Computer Science, Master's Programme (N2COS)
2. Mathematical Sciences, Master's Programme (N2MAT)

The course is a also a single-subject course at Gothenburg University.

To be eligible for the course, students must either have a bachelor's degree of 180 hec in Computer Science (or equivalent), or have successfully completed courses corresponding to 105 hec within the subjects Computer Science and Mathematics. There is also a specific subject requirement: 7.5 hec in discrete mathematics (for example DIT980 Discrete Mathematics for Computer Scientists or the sub-course Introductory Algebra of MMG200 Mathematics 1).

Applicants must prove knowledge of English: English 6/English level 2 or the equivalent level of an internationally recognized test, for example TOEFL, IELTS.

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.

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, undecidability
and expressiveness of predicate logic, plus an introduction to model checking: Linear-time temporal logic (LTL) and Branching-time temporal logic (CTL).

After completion of the course the student should be able to:

Knowledge and Understanding

• explain when a 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

Skills and Abilities

• 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 valid or not
• specify properties of a reactive system using linear-time temporal logic and branching-time temporal logic

Judgement Ability and Approach

• judge the relevance of logical reasoning in computer science, i.e. for modelling computer systems
• analyse the applicability of logical methods to solve problems in computer science, i.e. finding bugs with the use of model checking

The course consists of lectures, exercise sessions and non-obligatory assignments.

Language of instruction: English

The course is examined by an individual written hall exam at the end of the course.

There will be non-obligatory individual assignments offered during the course which grant bonus points for the written exam. These bonus points are valid during the whole academic year.

If a student who has been failed twice for the same examination element wishes to change examiner before the next examination session, such a request is to be granted unless there are specific reasons to the contrary (Chapter 6 Section 22 HF).

If a student has received a certificate of disability study support from the University of Gothenburg with a recommendation of adapted examination and/or adapted forms of assessment, an examiner may decide, if this is consistent with the course’s intended learning outcomes and provided that no unreasonable resources would be needed, to grant the student adapted examination and/or adapted forms of assessment.

If a course has been discontinued or undergone major changes, the student must be offered at least two examination sessions in addition to ordinary examination sessions. These sessions are to be spread over a period of at least one year but no more than two years after the course has been discontinued/changed. The same applies to placement and internship (VFU) except that this is restricted to only one further examination session.

If a student has been notified that they fulfil the requirements for being a student at Riksidrottsuniversitetet (RIU student), to combine elite sports activities with studies, the examiner is entitled to decide on adaptation of examinations if this is done in accordance with the Local rules regarding RIU students at the University of Gothenburg.

Sub-courses

1. Written hall examination, 7.5 credits
   Grading scale: Pass with distinction (5), Pass with credit (4), Pass (3) and Fail (U)

The final grade of the course is based on the result of the written exam.

The course is evaluated through meetings both during and after the course between teachers and student representatives. Further, an anonymous questionnaire is used to ensure written information. The outcome of the evaluations serves to improve the course by indication which parts could be added, improved, changed or removed.

The course is a joint course together with Chalmers.

The course replaces the course DIT202 Logic in Computer Science, 7.5 credits. The course cannot be included in a degree which contains DIT202. Neither can the course be included in a degree which is based on another degree in which the course DIT202 is included.