DD1350 Logic for Computer Science 6.0 credits

• Educational level

  First cycle

• Academic level (A-D)

  A

• Subject area

  Techonology
  

• Grade scale

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

• Course web page

• Course page on KTH Social

Learning outcomes

The overall aim of the course is to expose the students to mathematical logic and its use within theoretical computer science. The main focus of the course is on mastering the various proof techniques needed in other courses later in the curriculum.

After the course, the successful student will be able to:
- express informal statements in propositional and first-order predicate logic,
- argue for the correctness of a given proof calculus by relating appropriately its syntax and semantics,
- apply natural deduction for proving statements in first-order predicate logic,
- axiomatize abstract data types,
- perform proofs by well-founded and structural induction,
- perform proofs by co-induction,
- perform simple verifications based on temporal logic.

Course main content

A. Propositional logic
- Syntax and semantics
- Informal mathematical argumentation
- Application: Paradoxes and problem solving
- Boolean algebra
- Formal proof methods: Natural deduction, resolution
- Soundness, completeness and decidability

B. Predicate logic
- Syntax and semantics
- Proof methods: Natural deductio
- Completeness and decidability: Gödel's theorems
- Application: Program verification

C. First order theories
- Theories and axiomatisation
- Application: Algebraic data types

D. Proof by induction
- Well-founded induction
- Inductive definitions and structural induction
- Co-induction

E. Modal and temporal logic
- Syntax and semantics: Kripke structures
- Proof methods: Model checking
- Application: Parallel processes

Disposition

Lecutres: 30 h
Tutorials: 14 h
Laboratory assignments: 8 h

Eligibility

For single course students: completed upper secondary education including documented proficiency in Swedish corresponding to Swedish B, English corresponding to English A. Furthermore: 7,5 hp in mathematics and 6 hp in computer science or programming technics.

Prerequisites

For those already studying at KTH: DD1340 Introduction to Computer Science. At least two of the courses SF1612 Mathematic, Basic Course, SF1625 Calculus in One Variable and SF1604 Linear Algebra. Furthermore we recommend DD1361 Programming Paradigms (can be taken at the same time as this course).

Literature

The course literature is announced at least 4 weeks before the course starts at course web page.

Examination

• LAB1 - Laboratory work, 2.0 credits, grade scale: P, F
• TEN1 - Examination, 4.0 credits, grade scale: A, B, C, D, E, FX, F

Lab assignment 1: Resolution and logic programming Lab assignment 2: Implementation of database query systems

Requirements for final grade

Laboratory assignments (LAB1; 2 cr)
Examination (TEN1; 4 cr)

Offered by

CSC/Computer Science

Contact

Dilian Gurov, tel: 790 8198, e-post: dilian@csc.kth.se

Examiner

Dilian Gurov <dilian@kth.se>

Supplementary information

The course cannot be counted in the degree if the student has taken SF1642 or 5B1928.

Version

Course plan valid from: Autumn 09.
Examination information valid from: Spring 09.