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.

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

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.