DM846: Logic for Computer Science

Study Board of Science

Teaching language: Danish or English depending on the teacher, but English if international students are enrolled
EKA: N340037102, N340037112
Censorship: Second examiner: Internal, Second examiner: None
Grading: 7-point grading scale, Pass/Fail
Offered in: Odense
Offered in: Spring
Level: Master's level course approved as PhD course

STADS ID (UVA): N340037101
ECTS value: 10

Date of Approval: 02-10-2019


Duration: 1 semester

Version: Approved - active

Comment

15016601 (former UVA) is identical with this course description. 

Entry requirements

None

Academic preconditions

The student is expected to have basic understanding of mathematical proofs and to be familiar with the basics of propositional logic and predicate calculus, obtainable e.g. by having followed DM535 Discrete methods for computer science or MM537 Introduction to Mathematical Methods.

Course introduction

The aim of this course is to provide students with a background on logic focusing on aspects most relevant to computer science.

Expected learning outcome

At the end of this course, the student is expected to have the following competences:
  • understand the theoretical concepts of soundness, completeness, and decidability
  • prove soundness of particular logics
  • choose the logic framework most suited for particular computer science applications
  • be able to use existing tools for reasoning within particular logics

Content

  • deductive systems for propositional logic
  • first order logic and subsets thereof, combinatorial logic and type theory
  • Curry-Howard isomorphism
  • modal and temporal logic
  • formal specification and validation
  • pi-calculus, tools for logic reasoning

Literature

See itslearning for syllabus lists and additional literature references.

Examination regulations

Exam element b)

Timing

June

Tests

Oral exam

EKA

N340037102

Censorship

Second examiner: Internal

Grading

7-point grading scale

Identification

Student Identification Card

Language

Normally, the same as teaching language

Duration

30 minutes

Examination aids

To be announced during the course 

ECTS value

7

Additional information

Project followed by oral exam. The student completes a project and submits a report. The evaluation is based on the report and an oral exam, where the project is presented and the teacher asks about both the project and other topics covered in the course. 

The examination form for re-examination may be different from the exam form at the regular exam.

Exam element a)

Timing

Spring

Tests

Mandatory assignments

EKA

N340037112

Censorship

Second examiner: None

Grading

Pass/Fail

Identification

Full name and SDU username

Language

Normally, the same as teaching language

Examination aids

To be announced during the course 

ECTS value

3

Additional information

The examination form for re-examination may be different from the exam form at the regular exam.

Indicative number of lessons

62 hours per semester

Teaching Method

The teaching method is based on three phase model.
  • Intro phase: 42 hours
  • Skills training phase: 20 hours, hereof tutorials: 20 hours

Teacher responsible

Name E-mail Department
Luís Cruz-Filipe lcf@imada.sdu.dk Institut for Matematik og Datalogi, Datalogi, Artificial Intelligence, Cybersecurity, and Programming Languages

Additional teachers

Name E-mail Department City
Marco Peressotti Peressotti@imada.sdu.dk Institut for Matematik og Datalogi, Datalogi, Artificial Intelligence, Cybersecurity, and Programming Languages

Timetable

Administrative Unit

Institut for Matematik og Datalogi (datalogi, fiktiv)

Team at Registration & Legality

NAT

Recommended course of study

Profile Programme Semester Period