DV4: Datavetenskaplig logik, 7,5 hp

Innehåll

Logik i olika former genomsyrar hela datavetenskapen. Den används för att strukturera och söka i databaser, klassificera beräkningsproblem, verifiera att hård- och mjukvarusystem är korrekta och strukturera kunskap i intelligenta system, bara för att nämna några tillämpningar. Denna kurs syftar till att förmedla grunderna inom några av de logiska formalismer som används mest inom datavetenskapen, samt till att illustrera deras användningsområden. Kursen tar upp syntax och semantik för satslogik, första ordningens logik samt temproallogik. Inom satslogiken behandlas även bevisregler och konjunktiv normalform. Kursen behandlar också logikens roll inom ett antal datavetenskapliga områden och exemplifierar aktuell forskning inom området.

Kursen är uppdelad i två moduler. Modul 1: Teori (6,5 hp) och Modul 2: Litteraturstudie (1,0 hp).
 

Förväntade studieresultat

Kunskap och förståelse
Efter avslutad kurs ska studenten kunna

• (FSR 1) översiktligt redogöra för hur logik används i databassystem, automatisk verifiering, komplexitetsteori, artificiell intelligens och logikprogrammering samt kunna exemplifiera hur logik används inom andra datavetenskapliga områden,
• (FSR 2) redogöra för och använda sig av grundläggande begrepp och definitioner inom satslogik och första ordningens logik ,
• (FSR 3) redogöra för beräkningsproblemet SAT och Cook-Levins sats,
• (FSR 4) redogöra för de viktigaste principerna bakom moderna SAT-lösare och hur dessa kan användas i praktiken,
• (FSR 5) redogöra för de grundläggande principerna för temporallogik och dess roll inom automatisk verifiering,

Färdighet och förmåga

• (FSR 6) konstruera första ordningens formler för enkla egenskaper hos strängar och grafer samt exemplifiera första ordningens logiks begränsningar över dessa klasser av strukturer,
• (FSR 7) praktiskt avgöra om en satslogisk formel är tautologisk, motsägelsefull, eller satisfierbar,
• (FSR 8) praktiskt använda sig av bevisregler för satslogik, till exempel för att omvanda formler till konjunktiv normalform,
• (FSR 9) genomföra en mindre litteraturstudie syftande till att identifiera frågeställningar inom datavetenskaplig logik.

Behörighetskrav

För tillträde till kursen krävs kursen DV3: Beräkningar och språk och Introduktion till diskret matematik eller motsvarande kunskaper.

Undervisningens upplägg

Undervisningen bedrivs i form av föreläsningar, seminarier och övningar i mindre grupper. Utöver schemalagda aktiviteter krävs även individuellt arbete med materialet.

Examination

Examinationen på Modul 1 (FSR 1-8) sker dels genom ett antal mindre delprov samt en skriftlig salstentamen. Modulen bedöms med något av betygen Väl godkänd (VG), Godkänd (G) eller Underkänd (U).

Modul 2 (FSR 9) examineras genom ett antal obligatoriska uppgifter. Modulen bedöms med något av betygen Underkänd (U) eller Godkänd (G).

På hela kursen ges något av betygen Väl godkänd (VG), Godkänd (G) eller Underkänd (U). För att bli godkänd på hela kursen krävs godkänt betyg på båda modulerna. Betyget på kursen sätts till samma som betyget på Modul 1.

Anpassad examination
Examinator kan besluta om avsteg från kursplanens examinationsform. Individuell anpassning av examinationsformen ska övervägas utifrån studentens behov. Examinationsformen anpassas inom ramen för kursplanens förväntade studieresultat. Student som har behov av en anpassad examination ska senast 10 dagar innan examinationen begära anpassning hos Institutionen för datavetenskap. Examinator beslutar om anpassad examination som sedan meddelas studenten.

Övriga föreskrifter

Kursen får inte tas med i en examen tillsammans med kursen Grundläggande logik och modellteori (5DV102) till sitt fulla poängtal.

Om kursplanen har upphört att gälla eller kursen slutat erbjudas garanteras en student som någon gång registrerats på kursen minst tre provtillfällen (inklusive ordinarie provtillfälle) enligt denna kursplan under en tid av maximalt två år från det att kursplanen upphört att gälla eller kursen slutat erbjudas.