Kursen tar upp satslogik, predikatlogik och modellteori. Under kursen behandlas begrepp som syntax, semantik, bevis, sundhet och fullständighet, likhet, Horn-formler, unifiering och resolution.
Det krävs förtrogenhet med formella logiska system för att förstå grundläggande begrepp inom många datavetenskapliga områden såsom databaser, vetenskapliga beräkningar och maskininlärning. Modul 1 skapar den här förtrogenheten genom att förmedla logikens begrepp och tekniker ur en datavetenskaplig synvinkel.
Särskild vikt läggs på (i) skillnaden mellan logiskt sanna påståenden och bevis, dvs. definitionen av begreppet logisk sanning å ena sidan och utvecklandet av formella system för att härleda sanningsvärdet av ett påstående å andra sidan, (ii) algoritmiska aspekter på bevissystem med tonvikt på resolution och (iii) modeller för logiska system och hur dessa används för att verifiera egenskaper.
Modul 2 ger färdighetsträning inom logik genom ett antal obligatoriska uppgifter. Modulen illustrerar teori från modul 1, exempelvis genom uppgifter i logikprogrammering och ger studenten möjligheten att använda definitioner, notationer och formella system i praktiken.
Förväntade studieresultat
Efter avslutad kurs ska studenten kunna: Kunskap och förståelse
förklara skillnaden och samspelet mellan syntax och semantik (FSR 1)
förklara grundläggande begrepp, definitioner och notationer inom satslogik, predikatlogik och modellteori (FSR 2)
visa en grundläggande förståelse för satslogiska bevissystem (FSR 3)
redogöra för begreppen sundhet och fullständighet inom bevissystem (FSR 4)
definiera och använda sig av Hornklausuler (FSR 5)
uppvisa goda kunskaper och praktiska förmågor kring resolution, inbegripande att kunna omvandla formler till CNF, redogöra för resolutionsregeln, utföra substitution och unifiering, beräkna mest generella unifieraren samt utföra resolutionsbevis (FSR 6)
diskutera satisfierbarhet, sundhet och fullständighet för resolution både inom satslogik och predikatlogik (FSR 7)
definiera vad som menas med en modell för de olika logiska system som behandlats i kursen (FSR 8)
Färdighet och förmåga
Analysera och jämföra uttrycksfullheten i de olika logiska systemen som behandlas under kursen (FSR 9)
visa en grundläggande förståelse för hur modeller kan användas inom olika typer av verifikation (FSR 10)
använda sig av grundläggande begrepp, definitioner och notationer inom satslogik, predikatlogik och modellteori (FSR 11)
praktiskt använda sig av bevisregler och axiom (FSR 12)
Behörighetskrav
Univ:För tillträde till kursen krävs 7.5hp inom diskret matematik (tex Introduktion till diskret matematik, 5MA143) och en grundläggande kurs i programmeringsmetodik om minst 7.5hp (tex 5DV157, 5DV158, 5DV176 eller 5DV177) eller motsvarande kunskaper.
Undervisningens upplägg
Undervisningen bedrivs i form av föreläsningar, quizzar, programmeringsuppgifter samt övningar i mindre grupperUtöver schemalagda aktiviteter krävs även individuellt arbete med materialet.
Examination
Examinationen på den teoretiska modulen (FSR 1-12) sker genom ett skriftligt prov. På modul 1 sätts något av betygen Underkänd (U), Godkänd (3), Icke utan beröm godkänd (4) eller Med beröm godkänd (5).
Examinationen på den praktiska modulen (FSR 1-12) sker genom ett antal obligatoriska uppgifter som utförs individuellt enligt givna instruktioner. Antalet obligatoriska uppgifter kan variera mellan olika kurstillfällen och beror på deras omfattning men är aldrig mer än 5. På modulen ges betygen Underkänd (U) eller Godkänd (G).
På hela kursen ges något av betygen Underkänd (U), Godkänd (3), Icke utan beröm godkänd (4) eller Med beröm godkänd (5). För att bli godkänd på hela kursen krävs att samtliga prov och obligatoriska moment är godkända. Betyget på kursen är detsamma som det som satts på modul 1.
För studerande som inte godkänns vid ordinarie provtillfälle anordnas ytterligare provtillfälle.
Studerande som godkänts i ett prov får inte undergå förnyat prov för att få ett högre betyg. 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 för Institutionen för datavetenskap.
Examination baserad på denna kursplan garanteras under två år efter studentens förstagångsregistrering på kursen. Detta gäller även om kursen lagts ned och denna kursplan upphört gälla.
Avsteg från kursplanens examinationsform kan göras för en student som har beslut om pedagogiskt stöd på grund av funktionsnedsättning. Individuell anpassning av examinationsformen ska övervägas utifrån studentens behov. Examinationsformen anpassas inom ramen för kursplanens förväntade studieresultat. Efter begäran av studenten ska kursansvarig lärare, i samråd med examinator, skyndsamt besluta om anpassad examinationsform. Beslutet ska sedan meddelas studenten.
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.
