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 mjukvarudesign är korrekt 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 (översiktligt) monadisk andra ordningens logik och 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 består av två moment:
Moment 1: Teori 6.5 högskolepoäng
Moment 2 : Litteraturstudie 1 högskolepoäng

Förväntade studieresultat

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

• ö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 1),
• redogöra för och använda sig av grundläggande begrepp och definitioner inom satslogik, första ordningens logik och monadisk andra ordningens logik (FSR 2),
• redogöra för beräkningsproblemet SAT och Cook-Levins sats (FSR 3),
• redogöra för de viktigaste principerna bakom moderna SAT-lösare och hur dessa kan användas i praktiken (FSR 4),
• redogöra för de grundläggande principerna för temporallogik och dess roll inom automatisk verifiering (FSR 5),

Färdighet och förmåga

• 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 6),
• översätta en deterministisk finit automat till en motsvarande monadisk andra ordningens formel (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),
• konstruera monadiska andra ordningens formler för enkla egenskaper hos strängar (FSR 10),
• genomföra en mindre litteraturstudie syftande till att identifiera några aktuella frågeställningar inom datavetenskaplig logik (FSR 11).

Behörighetskrav

För tillträde till kursen krävs kursen DV3: Beräkningar och språk (5DV162) och Introduktion till diskret matematik (5MA143) 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å Moment 1 (FSR 1-10) sker dels genom ett antal mindre delprov samt en skriftlig tentamen. Momentet bedöms med något av betygen Väl godkänd (VG), Godkänd (G) eller Underkänd (U).

Moment 2 (FSR 11) examineras genom ett antal obligatoriska uppgifter. På moment 2 ges 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 att samtliga prov och obligatoriska moment är godkända. Betyget utgör en sammanfattande bedömning av resultaten vid examinationens olika delar och sätts först när alla obligatoriska moment är godkända.

Studerande som godkänts i ett prov får inte undergå förnyat prov för att få ett högre betyg

För studerande som inte godkänns vid ordinarie provtillfälle anordnas ytterligare provtillfälle. En student som utan godkänt resultat har genomgått två prov för en kurs eller en del av en kurs, har rätt att få en annan examinator utsedd, om inte särskilda skäl talar emot det (HF 6 kap. 22 §). Begäran om ny examinator ställs till prefekten vid Institutionen för datavetenskap.

Övriga föreskrifter

TILLGODORÄKNANDE
Student har rätt att få prövat om tidigare utbildning eller motsvarande kunskaper och färdigheter förvärvade i yrkesverksamhet kan tillgodoräknas för motsvarande utbildning vid Umeå universitet. Ansökan om tillgodoräknande skickas in till Studentcentrum/Examina. Mer information om tillgodoräknande finns på Umeå universitets studentwebb, www.student.umu.se, och i högskoleförordningen (6 kap). Ett avslag på ansökan om tillgodoräknande kan överklagas (Högskoleförordningen 12 kap) till Överklagandenämnden för högskolan. Detta gäller såväl om hela som delar av ansökan om tillgodoräknande avslås.

I en examen får denna kurs ej ingå, helt eller delvis, samtidigt med en annan kurs med likartat innehåll. Vid tveksamheter bör den studerande rådfråga studievägledare vid Institutionen för datavetenskap och/eller programansvarig för sitt program.

Speciellt gäller att denna kurs kan ej ingå fullt ut i en examen samtidigt som kursen Grundläggande logik och modellteori (5DV102).

Överlappet mellan denna och kurserna uppräknade ovan motsvarar ca 3 hp. Om man läst kursen ovan och vill tillgodoräkna de kunskaperna till denna så måste man komplettera med examinerande delar som motsvarar FSR 3-4, och 11.