DD1351 Logik för dataloger 7,5 hp

Logic for Computer Scientists

Kursen ger en introduktion till matematisk logik och dess tillämpningar inom datalogi, inklusive logikprogrammering.

  • Utbildningsnivå

    Grundnivå
  • Huvudområde

    Teknik
  • Betygsskala

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

Kurstillfällen/kursomgångar

HT19 logik19 för programstuderande

HT18 logik18 för programstuderande

Lärandemål

Efter godkänd kurs ska studenten kunna:

  • specificera allmänna egenskaper hos matematisk-datalogiska strukturer och bevisa dessa med hjälp av naturlig deduktion i satslogik och predikatlogik,
  • specificera induktiva definitioner hos datastrukturer och bevisa dessa med strukturell induktion,
  • specificera och bevisa systemegenskaper med hjälp av temporal logik,
  • specificera och bevisa programegenskaper med hjälp av Hoarelogik,
  • tillämpa metoder för automatisk deduktion och utföra enkla bevis med modellprövning,
  • tillämpa och förklara grundläggande begrepp inom logikprogrammering: unifiering, backtracking, snitt, negering och olika programmeringstekniker som t.ex. generate-test

i syfte att

  • behärska de bevistekniker som behövs i kommande kurser i utbildningen.

För högre betyg ska studenten dessutom kunna:

  • argumentera för korrektheten hos en viss bevisteknik: sundhet och fullständighet,
  • argumentera för bevisteknikers lämplighet till automatisk deduktion: avgörbarhet.

Kursens huvudsakliga innehåll

A. Satslogik

- Informell matematisk argumentation
- Formella bevismetoder: naturlig deduktion
- Syntax och semantik
- Sundhet, fullständighet och avgörbarhet

B. Predikatlogik

- Syntax och semantik, Kripke-strukturer
- Bevismetoder: naturlig deduktion
- Sundhet, fullständighet och oavgörbarhet, Gödels satser

C. Prolog

- Resolution och logikprogrammering: unifiering, backtracking, negering, snitt och låddiagram

D. Induktionsbevis

- Matematisk och fullständig induktion
- Induktiva definitioner och strukturell induktion

E. Temporallogik

- Syntax och semantik
- Bevismetoder: modellprövning

F. Hoare-logik

- Programsemantik och programspecifikation
- Programverifikation
- Syntax och semantik: Kripke-strukturer
- Bevismetoder: modellprövning

Behörighet

DD1337 Programmering och DD1338 Algoritmer och datastrukturer, eller motsvarande kurser. Minst två av kurserna SF1671 Matematik baskurs med diskret matematik, SF1625 Envariabelanalys och SF1624 Algebra och geometri eller motsvarande kurser.

Rekommenderade förkunskaper

DD1337 Programmering, DD1338 Algoritmer och datastrukturer, SF1671 Matematik baskurs med diskret matematik, SF1625 Envariabelanalys och SF1624 Algebra och geometri eller motsvarande kurser.

Litteratur

Meddelas senast 10 veckor före kursstart på kurswebben.

Examination

  • LAB1 - Laborationer, 1,5, betygsskala: P, F
  • LAB2 - Laborationer, 2,0, betygsskala: P, F
  • TEN1 - Tentamens, 4,0, betygsskala: A, B, C, D, E, FX, F

I denna kurs tillämpas skolans hederskodex, se: http://www.kth.se/csc/utbildning/hederskodex.

Vid särskilda skäl för studenter med funktionsnedsättning och vid omexamination av enstaka studenter kan examinatorn medge annan examinationsform.

Plussning är tillåtet.

Ges av

EECS/Datavetenskap

Kontaktperson

Johan Karlander <karlan@kth.se>

Examinator

Johan Karlander <karlan@kth.se>

Övrig information

Kursen kan inte kombineras med DD1350 eller SF1642.

Påbyggnad

DD1362 Programmeringsparadigm, ID2213 Logikprogrammering.  

Versionsinformation

Kursplan gäller från och med VT2019.
Examinationsinformation gäller från och med VT2019.