DD1350 Logik för dataloger 6,0 hp

Logic for Computer Science

Kursen ger en introduktion till matematisk logik och dess tillämpningar inom datalogi. Du får lära dig:

  • använda logik för att formalisera egenskaper hos datastrukturer, algoritmer och systemegenskaper
  • genomföra bevis för att härleda slutsatser utifrån givna premisser
  • behärska olika bevistekniker, såsom naturlig deduktion, induktion. s.k. Hoare-logik för programverifikation, och temporal-logik för systemverifikation
  • förstå hur logiska formler kan ges en precis matematisk (modell-teoretisk) innebörd
  • behärska grunderna för automatisk deduktion
  • förstå och argumentera kring viktiga egenskaper hos bevissystem, såsom sundhet, fullständighet och avgörbarhet
  • Utbildningsnivå

    Grundnivå
  • Huvudområde

    Teknik
  • Betygsskala

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

Det finns inget planerat kurstillfälle.

Lärandemål

Efter kursen skall studenterna kunna:

  • specificera och bevisa:
    • allmänna egenskaper hos matematisk-datalogiska strukturer:
      • naturlig deduktion i satslogik och predikatlogik
      • ge induktiva definitioner och genomföra bevis med strukturell induktion
    • systembeteendeegenskap: temporal logik
    • programegenskap: Hoares logik
  • argumentera för korrektheten hos en viss bevisteknik: sundhet och fullständighet
  • argumentera för bevisteknikers lämplighet till automatisk deduktion: avgörbarhet
  • tillämpa metoder för automatisk deduktion:
    • utföra enkla bevis med modellprövning

för att

  • lära sig behärska de bevistekniker som kommer att behövas i kommande kurser i utbildningen.

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

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
- Tillämpning: Parallella processer

Kursupplägg

Föreläsningar: 30 h
Övningar: 14 h
Laborationer: 8 h

Behörighet

För fristående kursstuderande: grundläggande högskolebehörighet samt 7,5 hp i matematik och 6 hp datalogi eller programmeringsteknik. Dessutom krävs svenska B eller motsvarande och engelska A eller motsvarande.

Rekommenderade förkunskaper

För KTH-studerande: DD1340 Introduktion till datalogi. Minst två av kurserna SF1612 Matematik baskurs, SF1625 Envariabelanalys och SF1604 Linjär algebra. Dessutom rekommenderas DD1361 Programmeringsparadigm (kan läsas parallellt med kursen).

Litteratur

Michael Huth, Mark Ryan "Logic in Computer Science"
Cambridge University Press 2004 (2nd edition)
ISBN 0 521 54310X

Examination

  • LAB1 - Laborationer, 2,0, betygsskala: P, F
  • TEN1 - Tentamen, 4,0, betygsskala: A, B, C, D, E, FX, F

Laboration1: Logikprogrammering
Laboration2: Temporallogik och modellprovning

Krav för slutbetyg

Laborationer (LAB1; 2 hp)
Tentamen (TEN1; 4 hp)

Ges av

EECS/Datavetenskap

Kontaktperson

Johan Karlander (karlan@kth.se)

Examinator

Johan Karlander <karlan@kth.se>

Övrig information

Den här kursen får inte räknas med i examen om studenten har läst SF1642 eller 5B1928.

Versionsinformation

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