Kursplan fastställd 2025-02-20 av programansvarig (eller motsvarande).
Kursöversikt
- Engelskt namnLogic in computer science
- KurskodDAT060
- Omfattning7,5 Högskolepoäng
- ÄgareMPALG
- UtbildningsnivåAvancerad nivå
- HuvudområdeDatateknik, Informationsteknik
- InstitutionDATA- OCH INFORMATIONSTEKNIK
- BetygsskalaTH - Mycket väl godkänd (5), Väl godkänd (4), Godkänd (3), Underkänd
Kurstillfälle 1
- Undervisningsspråk Engelska
- Anmälningskod 02135
- Sökbar för utbytesstudenterJa
Poängfördelning
Modul | LP1 | LP2 | LP3 | LP4 | Sommar | Ej LP | Tentamensdatum |
---|---|---|---|---|---|---|---|
0106 Tentamen 7,5 hp Betygsskala: TH | 7,5 hp |
I program
- MPALG - Datavetenskap - algoritmer, programspråk och logik, Årskurs 1 (obligatorisk)
- MPCSN - Datorer, nätverk och system, Årskurs 2 (valbar)
Examinator
- Ana Bove
- Enhetschef, Computing Science, Data- och informationsteknik
Behörighet
Grundläggande behörighet för avancerad nivåSökande med en programregistrering på ett program där kursen ingår i programplanen undantas från ovan krav.
Särskild behörighet
Engelska 6Sökande med en programregistrering på ett program där kursen ingår i programplanen undantas från ovan krav.
Kursspecifika förkunskaper
Kravet för kursen är att ha framgångsrikt slutfört två år med ämnet datavetenskap eller motsvarande. Särskilt relevant är matematik (inklusive diskret matematik), programmering, algoritmer och/eller datastrukturer.Syfte
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.Lärandemål (efter fullgjord kurs ska studenten kunna)
Efter godkänd kurs ska studenten kunna:
- 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 predikatkalkyl
- förklara hur man kontrollerar om en linjär och en branching-time temporallogik temporär logisk formel är giltig i en given modell
- 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
- 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
Innehåll
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: linjär temporallogik (LTL) och branching-tid temporallogik (CTL).Organisation
Undervisning ges i form av föreläsningar, övningar och frivillig inlämningsuppgift som ger bonus poäng på tentamen.Litteratur
Huth, Ryan. Logic in Computer Science, 2nd Edition, se https://www.chalmersstore.se/en/e-books/e-book-logic-in-computer-science.htmlExamination inklusive obligatoriska moment
Kursen examineras genom en individuell skriftligsalstentamen i slutet av kursen.Frivilliga inlämningsuppgifter som ger bonus poäng på tentamen erbjuds under kursen. Bonus poänger gäller under hela akademiska året.
Kursens examinator får examinera enstaka studenter på annat sätt än vad som anges ovan om särskilda skäl föreligger, till exempel om en student har ett beslut från Chalmers om riktat pedagogiskt stöd på grund av funktionsnedsättning.