Matematisk logik för datavetenskap

Kursen kan ingå i följande program:

1. Computer Science, masterprogramme (N2COS)
2. Matematiska vetenskaper, masterprogram (N2MAT)

Kursen ges även som fristående kurs vid Göteborgs Universitet.

För att vara behörig till kursen måste studenten antingen ha en kandidatexamen om 180 hp i datavetenskap (eller motsvarande), eller ha framgångsrikt slutfört kurser motsvarande 105 hp inom ämnena datavetenskap och matematik. Det finns även ett särskilt ämneskrav: 7,5 hp i diskret matematik (till exempel DIT980 Diskret matematik för Datavetare eller delkursen Inledande algebra från MMG200 Matematik 1).

Följande kunskapsnivå i Engelska krävs: Engelska 6/Engelska nivå 2 eller motsvarande från ett erkänt internationellt test, t.ex. TOEFL, IELTS.

Kraftfulla verktyg för verifikation av programvaru- och hårdvarusystem utvecklats. Dessa verktyg förlitar sig på ett avgörande sätt i logiska tekniker. Kursen ger en sund grund i logik och en kort introduktion till några logiska ramverk som används för att modellera, specificera och verifiera datorsystem. Grundläggande kunskaper i logik är en god grund för kurser i programverifiering, formella metoder och artificiell intelligens.

Kursen täcker sats- och predikatkalkyl och modellkontrol (model checking). Mer konkret ger kursen en grundlig introduktion till grundläggande begrep inom logik såsom naturlig deduktion, semantik för både sats- och predikatkalkyl, sundhet och fullständighet, konjunktiva normalformer, oavgörbart och uttrycksfullhet av predikatlogik, samt en introduktion till modellkontroll (model checking): linjär temporallogik (LTL) och branching-tid temporallogik (CTL).

Efter godkänd kurs ska studenten kunna:

Kunskap och förståelse

• förklara när en formel är en tautologi
• förklara begreppet modell för ett första ordningens språk och för temporallogik
• förklara när en första ordningens och en temporallogiks formel är semantiskt giltigt
• förklara betydelsen av sundhet och fullständighet teoremen för sats- och predikatkalky
• förklara hur man kontrollerar om en linjär och en branching-time temporallogik formel är giltig i en given modell

Färdigheter och förmåga

• skriva och kontrollera härledningar i naturlig deduktion för sats- och predikatkalkyl
• tillämpa sundhet och fullständighet teoremen för att argumentera för korrektheten av vissa bevis
• argumentera semantiskt om en given formel är giltig eller inte
• specificera egenskaper hos ett reaktivt system med hjälp av linjär temporallogik och branching-time temporallogik

Värderingsförmåga och förhållningssätt

• bedöma relevansen av logisk resonemang inom datavetenskap, dvs för modellering av datorsystem
• analysera användbarheten av logiska metoder för att lösa problem inom datavetenskap, dvs. hitta buggar med användning av modellkontroll

Undervisning ges i form av föreläsningar, övningar och frivillig inlämningsuppgift som ger bonus poäng på tentamen.

Undervisningsspråk: engelska

Kursen examineras genom en individuell skriftlig salstentamen i slutet av kursen.

Under kursen erbjuds icke-obligatoriska individuella inlämningar som ger bonuspoäng inför den skriftliga tentamen. Dessa bonuspoäng gäller under hela läsåret.

Om en student som har underkänts två gånger på samma examinerande moment önskar byta examinator inför nästa examinationstillfälle ska en sådan begäran bifallas om det inte finns särskilda skäl däremot (6 kap. 22 § HF).

Om en student har fått besked om pedagogiskt stöd från Göteborgs universitet med rekommendation om anpassad examination och/eller anpassad examinationsform kan examinator, i det fall det är förenligt med kursens lärandemål och förutsatt att inte orimliga resurser krävs, besluta att bevilja studenten anpassad examination och/eller anpassad examinationsform.

Om en kurs har avvecklats eller genomgått en större förändring ska studenten erbjudas minst två examinationstillfällen, utöver ordinarie examinationstillfälle. Dessa tillfällen fördelas under en tid av minst ett år, dock som längst två år efter det att kursen avvecklats/förändrats. Vad gäller praktik och verksamhetsförlagd utbildning (VFU) gäller motsvarande, men med begränsning till endast ett ytterligare examinationstillfälle.

Om en student har fått besked om att denne uppfyller kraven för att vara student vid Riksidrottsuniversitetet (RIU-student) har examinator rätt att besluta om anpassning vid examination, om detta görs i enlighet med Lokala regler gällande RIU-studenter vid Göteborgs universitet

Delkurser

1. Skriftlig salstentamen, 7,5 hp
   Betygsskala: Mycket väl godkänd (5), Väl godkänd (4), Godkänd (3) och Underkänd (U)

Slutbetyget i kursen baseras på betyget på den skriftliga salstentamen.

Kursen utvärderas genom möten, både under och efter kursen, mellan lärare och studentrepresentanter. Ett anonymt skriftligt frågeformulär skickas även ut till studenterna efter kursens slut. Resultaten av utvärderingarna används för att förbättra kursinnehållet och som indikation till vilka delar som skulle kunna läggas till, tas bort, förbättras eller ändras.

Kursen är samläst med Chalmers.

Kursen ersätter kursen DIT202 Matematisk logik för datavetenskap, 7,5 hp. Den här kursen kan inte ingå i en examen som innehåller DIT202. Den kan inte heller ingå i en examen som bygger på en annan examen där DIT202 ingår.