Logik för dataloger, 6 poäng
Aktuell/nästa kursomgång:
Höstterminen 2012, perioder 1+2
DD1350 Logik för dataloger
Kursbeskrivning
Kursen ger en introduktion till matematisk logik och dess
tillämpningar
inom teoretisk datalogi. Det huvudsakliga syftet är att
studenterna
lär sig behärska bevisteknikerna som används i kommande
kurser i utbildningen.
Studenterna skall lära sig
att:
- använda sig av logik för att formalisera allmänna egenskaper av datalogiska strukturer samt program- och systemegenskaper
- behärska olika bevistekniker:
- program- och systemverifikation
- behärska grunderna till automatisk
deduktion
Efter kursen skall
studenterna kunna:
- formalisera och genomföra bevis:
- av allmänna egenskaper av datalogiska strukturer:
- naturlig deduktion i
satslogik och predikatlogik
- motivera och genomföra bevis med strukturell induktion
- av programegenskaper: Hoares
logik
- av systemegenskaper: Temporallogik
- argumentera för korrektheten
hos en viss bevisteknik: sundhet
och fullständighet
- motivera och tillämpa metoder för automatisk deduktion:
- utföra enkla bevis med modelprövning
- argumentera för olika bevisteknikers lämplighet till automatisk deduktion: avgörbarhet
Kursansvarig
Kursansvarig är
Dilian Gurov, e-mail
dilian
at csc.kth.se, tel. 08-790 81 98.
Dilian hittar ni på plan 4, Osquars backe 2, rum 4417.
Extentor
DD1350