Skip to main content
Till KTH:s startsida Till KTH:s startsida

DD1351 Logic for Computer Scientists 7.5 credits

This course gives an introduction to mathematical logic and its use within computer science, including logic programming.

Choose semester and course offering

Choose semester and course offering to see current information and more about the course, such as course syllabus, study period, and application information.


For course offering

Autumn 2024 logik24 programme students

Application code


Headings with content from the Course syllabus DD1351 (Autumn 2021–) are denoted with an asterisk ( )

Content and learning outcomes

Course contents

A. Propositional logic

- Informal mathematical argumentation
- Formal proof techniques: natural deduction
- Syntax and semantics
- Soundness, completeness and decidability

B. Predicate logic

- Syntax and semantics, Kripke structures
- Proof techniques: natural deduction
- Soundness, completeness and undecidability, Gödel's theorems

C. Prolog

- Resolution and logic programming: unification, backtracking, negation, intersection and box diagrams

D. Inductive proof

- Mathematical and complete induction
- Inductive definitions and structural induction

E. Temporal logic

- Syntax and semantics
- Proof techniques: model checking

F. Hoare logic

- Program semantics and specification
- Program verification
- Syntax and semantics: Kripke structures
- Proof techniques: model checking

Intended learning outcomes

After passing the course, the students should be able to:

  • specify general properties of mathematical-computational structures and prove these by means of natural deduction in propositional logic and predicate logic,
  • specify inductive definitions of data structures and prove these with structural induction,
  • specify and prove system properties by means of temporal logic,
  • specify and prove program properties by means of Hoare logic,
  • apply methods for automatic deduction and carry out simple proofs with model checking,
  • apply and explain basic concepts in logic programming: unification, backtracking, intersection, negation and different programming techniques such as generate-test

in order to

  • master the proof techniques that are needed in future courses in the education.

For higher grades, the student should furthermore be able to:

  • argue for the correctness of a certain proof technique: soundness and completeness,
  • argue for the suitability of proof techniques to automatic deduction: decidability.

Literature and preparations

Specific prerequisites

  • Knowledge and skills in programming, 6 credits, corresponding to completed course DD1310/DD1311/DD1312/DD1314/DD1315/DD1316/DD1318/DD1321/DD1331/DD1337/DD100N/ID1018.
  • Knowledge in discrete mathematics, 3 credits, corresponding to completed course SF1671/SF1610/SF1630/SF1662/SF1679.

Active participation in a course offering where the final examination is not yet reported in Ladok is considered equivalent to completion of the course.

Registering for a course is counted as active participation.

The term 'final examination' encompasses both the regular examination and the first re-examination.

Recommended prerequisites

SF1625 Calculus in one variable, and SF1624 Algebra and geometry, or corresponding courses.


No information inserted


No information inserted

Examination and completion

If the course is discontinued, students may request to be examined during the following two academic years.

Grading scale

A, B, C, D, E, FX, F


  • HEM1 - Homework and quiz, 4.0 credits, grading scale: A, B, C, D, E, FX, F
  • LAB1 - Laboratory work, 1.5 credits, grading scale: P, F
  • LAB2 - Laboratory work, 2.0 credits, grading scale: P, F

Based on recommendation from KTH’s coordinator for disabilities, the examiner will decide how to adapt an examination for students with documented disability.

The examiner may apply another examination format when re-examining individual students.

Opportunity to complete the requirements via supplementary examination

No information inserted

Opportunity to raise an approved grade via renewed examination

No information inserted


Ethical approach

  • All members of a group are responsible for the group's work.
  • In any assessment, every student shall honestly disclose any help received and sources used.
  • In an oral assessment, every student shall be able to present and answer questions about the entire assignment and solution.

Further information

Course room in Canvas

Registered students find further information about the implementation of the course in the course room in Canvas. A link to the course room can be found under the tab Studies in the Personal menu at the start of the course.

Offered by

Main field of study


Education cycle

First cycle

Add-on studies

DD1362 Programming paradigms, ID2213 Logic programming.  


Johan Karlander

Transitional regulations

The previous course component TEN1 is replaced by HEM1.

Supplementary information

The course cannot be combined with DD1350, DD1361, or SF1642.

In this course, the EECS code of honor applies, see: