bild
Skolan för
datavetenskap
och kommunikation
KTH / CSC / Kurser / DD1350

Logik för dataloger, 6 poäng

Aktuell/nästa kursomgång: Höstterminen 2013, 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:
    • naturlig deduktion
    • induktion
    • 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 5, Osquars backe 2, rum 4520.


Extentor



Copyright © Sidansvarig: Dilian Gurov <dilian@csc.kth.se>
Uppdaterad 2013-08-22