DD1350 Logik för dataloger 6,0 hp
Denna kurs är avvecklad.
Sista planerade examination: VT 2021
Avvecklingsbeslut:
Ingen information tillagdInnehå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
- allmänna egenskaper hos matematisk-datalogiska strukturer:
- 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.
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
Kurslitteratur
Michael Huth, Mark Ryan "Logic in Computer Science"
Cambridge University Press 2004 (2nd edition)
ISBN 0 521 54310X
Examination och slutförande
När kurs inte längre ges har student möjlighet att examineras under ytterligare två läsår.
Betygsskala
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 handläggare av stöd till studenter med 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
Möjlighet till plussning
Examinator
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.
Ytterligare information
Kursrum i Canvas
Ges av
Huvudområde
Utbildningsnivå
Påbyggnad
Kontaktperson
Övrig information
Den här kursen får inte räknas med i examen om studenten har läst SF1642 eller 5B1928.