DD1351 Logic for Computer Scientists 7.5 credits

Logik för dataloger

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

Show course information based on the chosen semester and course offering:

Offering and execution

No offering selected

Select the semester and course offering above to get information from the correct course syllabus and course offering.

Course information

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.

Course Disposition

No information inserted

Literature and preparations

Specific prerequisites *

DD1337 Programming and DD1338 Algorithms and Data Structures or the equivalent courses. At least two of the courses SF1671 Mathematics Basic Course with Discrete Mathematics, SF1625 Calculus in One Variable and SF1624 Algebra and Geometry or the equivalent courses.

Recommended prerequisites

DD1337 Programming, DD1338 Algorithms and data structures, SF1671 Mathematics, basic course, with discrete mathematics, SF1625 Calculus in one variable, and SF1624 Algebra and geometry, or corresponding courses.

Equipment

No information inserted

Literature

Will be announced on the course web no later than 10 weeks before the start of the course.

Examination and completion

Grading scale *

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

Examination *

  • LAB1 - Laboratory work, 1.5 credits, Grading scale: P, F
  • LAB2 - 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.

In this course, the code of honor of the school is applied, see: http://www.kth.se/en/csc/utbildning/hederskodex

Under exceptional circumstances for students with disabilities and at re-examination of individual students, the examiner can admit other examination format.

Plussing (re-examination to raise a grade) is allowed.

Opportunity to complete the requirements via supplementary examination

No information inserted

Opportunity to raise an approved grade via renewed examination

No information inserted

Examiner

Johan Karlander

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 DD1351

Offered by

EECS/Computer Science

Main field of study *

Technology

Education cycle *

First cycle

Add-on studies

DD1362 Programming paradigms, ID2213 Logic programming.  

Contact

Johan Karlander karlan@kth.se

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.

Supplementary information

The course cannot be combined with DD1350 or SF1642.

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