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:

• specificera allmänna egenskaper hos matematisk-datalogiska strukturer och bevisa dessa med hjälp av naturlig deduktion i satslogik och predikatlogik,
• specificera induktiva definitioner hos datastrukturer och bevisa dessa med strukturell induktion,
• specificera och bevisa systemegenskaper med hjälp av temporal logik,
• specificera och bevisa programegenskaper med hjälp av Hoarelogik,
• tillämpa metoder för automatisk deduktion och utföra enkla bevis med modellprövning,
• tillämpa och förklara grundläggande begrepp inom logikprogrammering: unifiering, backtracking, snitt, negering och olika programmeringstekniker som t.ex. generate-test

i syfte att

• behärska de bevistekniker som behövs i kommande kurser i utbildningen.

För högre betyg ska studenten dessutom kunna:

• argumentera för korrektheten hos en viss bevisteknik: sundhet och fullständighet,
• argumentera för bevisteknikers lämplighet till automatisk deduktion: avgörbarhet.

• Kunskaper och färdigheter i programmering, 6 hp, motsvarande slutförd kurs  DD1310/DD1311/DD1312/DD1314/DD1315/DD1316/DD1318/DD1321/DD1331/DD1337/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 - Hemuppgifter och quiz, 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

Thomas Sjöland

• 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 om kursen kan hittas på kurswebben via länken nedan. Information på kurswebben kommer framöver flyttas till denna sida.

DD1362 Programmeringsparadigm, ID2213 Logikprogrammering.  

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