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

Kursomgång och genomförande

Kursomgångar saknas för tidigare och kommande terminer, samt för innevarande termin.

Kursinformation

Innehåll och lärandemål

Kursinnehå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

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.

Kursupplägg

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

Kurslitteratur och förberedelser

Särskild 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).

Utrustning

Ingen information tillagd

Kurslitteratur

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

Examination och slutförande

Betygsskala *

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

Examination *

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

Examinator beslutar, baserat på rekommendation från KTH:s samordnare för funktionsnedsättning, om eventuell anpassad examination för studenter med dokumenterad, varaktig funktionsnedsättning.

Examinator får medge annan examinationsform vid omexamination av enstaka studenter.

Laboration1: Logikprogrammering
Laboration2: Temporallogik och modellprovning

Övriga krav för slutbetyg *

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

Möjlighet till komplettering

Ingen information tillagd

Möjlighet till plussning

Ingen information tillagd

Examinator

Johan Karlander

Ytterligare information

Kurswebb

Ytterligare information om kursen kan hittas på kurswebben via länken nedan. Information på kurswebben kommer framöver flyttas till denna sida.

Kurswebb DD1350

Ges av

EECS/Datavetenskap

Huvudområde *

Teknik

Utbildningsnivå *

Grundnivå

Påbyggnad

Ingen information tillagd

Kontaktperson

Johan Karlander (karlan@kth.se)

Etiskt förhållningssätt *

  • Vid grupparbete har alla i gruppen ansvar för gruppens arbete.
  • Vid examination ska varje student ärligt redovisa hjälp som erhållits och källor som använts.
  • Vid muntlig examination ska varje student kunna redogöra för hela uppgiften och hela lösningen.

Övrig information

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