DD1351 Logik för dataloger 7,5 hp

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: unifiering, backtracking, negering, snitt och låddiagram

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

Efter godkänd kurs ska studenten kunna

• använda logik för att uttrycka formella egenskaper hos datastrukturer, algoritmer och datorsystem
• använda logikprogramspråket Prolog
• genomföra bevis för att härleda slutsatser utifrån givna premisser
• använda olika bevistekniker, såsom naturlig deduktion, induktion, s.k. Hoare-logik för programverifikation och temporallogik för systemverifikation
• formulera logiska formler för att ge en precis matematisk (modellteoretisk) innebörd av olika matematiska och datalogiska påståenden
• resonera kring viktiga egenskaper hos bevissystem, såsom sundhet, fullständighet och avgörbarhet
• motivera och tillämpa metoder för automatisk deduktion som att utföra enkla bevis med modellprövning

i syfte att

• behärska de bevistekniker som behövs i kommande kurser i utbildningen
• få ett bredare perspektiv på programmering.

Kunskaper och färdigheter i programmering, 6 hp, motsvarande slutförd kurs DD1337/DD1310-DD1319/DD1321/DD1331/DD1333/DD100N/ID1018.

Kunskaper i diskret matematik, 3 hp, motsvarande slutförd kurs SF1671/SF1610/SF1630/SF1662/SF1679.

Aktivt deltagande i kursomgång vars slutexamination ännu inte är Ladokrapporterad jämställs med slutförd kurs.
Den som är registrerad anses vara aktivt deltagande.
Med slutexamination avses både ordinarie examination och det första omexaminationstillfället.

SF1625 Envariabelanalys och SF1624 Algebra och geometri eller motsvarande kurser.

När kurs inte längre ges har student möjlighet att examineras under ytterligare två läsår.

• HEM1 - Hemuppgift och quizzar, 4,0 hp, betygsskala: A, B, C, D, E, FX, F
• LAB1 - Laborationer, 1,5 hp, betygsskala: P, F
• LAB2 - Laborationer, 2,0 hp, betygsskala: P, 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.

Johan Karlander

• 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.

Det tidigare momentet TEN1 ersätts av HEM1.

Kursen kan inte kombineras med DD1350, DD1361 eller SF1642.

I denna kurs tillämpas EECS hederskodex, se:
http://www.kth.se/eecs/utbildning/hederskodex