DD1351 · Kungliga Tekniska högskolan
Logik för dataloger
43 tentor15 ämnen
Kursinnehåll
Bevissystem
7 uppgifter · 3 teorikapitel
CTL
22 uppgifter
Induktion
5 uppgifter
Modeller
22 uppgifter
PL - Naturlig deduktion
35 uppgifter
Vad ingår?
0 uppgifter
Sorterat efter ämne och svårighet, direkt från tentor.
43 tentor med lösningar
Alla tidigare tentor samlade, öva på riktiga examensfrågor.
AI-handledare (KAI)
Få steg-för-steg-hjälp dygnet runt, skräddarsydd för den här kursen.
0 studieplaner
Personliga studieplaner som anpassar sig till dina framsteg.
Generera tester
Skapa anpassade övningstester baserat på ämne och svårighet.
Framstegsanalys
Se vad du vet, vad du behöver granska och vad som finns kvar.
HP
7.5
Språk
Svenska
Nivå
Grundnivå
Fakultet
Skolan för elektroteknik och datavetenskap
Institution
EECS/Datavetenskap
Lärandemål
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
- behärska de bevistekniker som behövs i kommande kurser i utbildningen
- få ett bredare perspektiv på programmering.
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: unifiering, backtracking, negering, snitt och låddiagram
- D. Induktionsbevis
- Matematisk och fullständig induktion
- Induktiva definitioner och strukturell induktion
- E. Temporallogik
- Bevismetoder: modellprövning
- F. Hoare-logik
- Programsemantik och programspecifikation
- Programverifikation
- Syntax och semantik: Kripke-strukturer
Förutsättningar
- 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.
Litteratur
Saknas
Liknande kurser vid andra universitet
Gör som 15 000+ studenter och ta kontroll över ditt tentaplugg.
Kom igång gratis