DD1350 Logik för dataloger 6,0 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

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

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

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.

Michael Huth, Mark Ryan "Logic in Computer Science"
Cambridge University Press 2004 (2nd edition)
ISBN 0 521 54310X

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

• 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

Laborationer (LAB1; 2 hp)
Tentamen (TEN1; 4 hp)

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.

Den här kursen får inte räknas med i examen om studenten har läst SF1642 eller 5B1928.