DD1350 Logic for Computer Science 6.0 credits
This course has been discontinued.
Last planned examination: Spring 2021
Decision to discontinue this course:
No information inserted
This course gives an introduction to mathematical logic and its use within computer science.
Content and learning outcomes
Course contents
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
Intended 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 disposition
Lecutres: 30 h
Tutorials: 14 h
Laboratory assignments: 8 h
Literature and preparations
Specific prerequisites
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.
Recommended 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).
Equipment
Literature
The course literature is announced at least 4 weeks before the course starts at course web page.
Examination and completion
If the course is discontinued, students may request to be examined during the following two academic years.
Grading scale
Examination
- LAB1 - Laboratory work, 2.0 credits, grading scale: P, F
- TEN1 - Examination, 4.0 credits, grading scale: A, B, C, D, E, FX, 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.
Lab assignment 1: Resolution and logic programming Lab assignment 2: Implementation of database query systems
Other requirements for final grade
Laboratory assignments (LAB1; 2 cr)
Examination (TEN1; 4 cr)
Opportunity to complete the requirements via supplementary examination
Opportunity to raise an approved grade via renewed examination
Examiner
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 web
Further information about the course can be found on the Course web at the link below. Information on the Course web will later be moved to this site.
Course web DD1350Offered by
Main field of study
Education cycle
Add-on studies
Contact
Supplementary information
The course cannot be counted in the degree if the student has taken SF1642 or 5B1928.
The course was given for the last time autumn 2017. It has been replaced by DD1351. Last possibility to be examined on DD1350 is spring 2021.