DD1351 Logic for Computer Scientists 7.5 credits

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

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

• use logic to express formal properties of data structures, algorithms and computer systems
• use the Prolog logic programming language
• conduct proofs to derive conclusions from given premises
• use different proof techniques, such as natural deduction, induction, Hoare logic for programme verification and temporal logic for system verification
• formulate logical formulae to give a precise mathematical (model-theoretic) meaning to various mathematical and computer science statements
• discuss important properties of evidence systems, such as soundness, completeness and decidability
• justify and apply methods of automatic deduction such as performing simple proofs with model checking

in order to

• master the proof techniques that are needed in future courses in the education
• obtain a broader perspective on programming.

Knowledge and skills in programming, 6 credits, equivalent to completed course DD1337/DD1310-DD 1319/DD1321/DD1331/DD1333/DD100N/ID1018.

Knowledge in discrete mathematics, 3 credits, equivalent to completed course SF1671/SF1610/SF1630/SF1662/SF1679.

Active participation in a second-cycle course offering where the final examination is not yet reported in LADOK is considered equivalent to completion of the course.
Being registered for a course counts as active participation.
The term 'final examination' encompasses both the regular examination and the first re-examination.

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

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

• HEM1 - Homework and quizzes, 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.

Johan Karlander

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

The earlier component TEN1 is replaced by HEM1.

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

In this course, the EECS code of honor applies, see:
http://www.kth.se/en/eecs/utbildning/hederskodex