Kursplan för Logik för datavetenskap

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

0106 Tentamen 7,5 hp
Betygsskala: TH		7,5 hp

I program

Examinator

Gå till kurshemsidan (Öppnas i ny flik)

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 6
Sö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:

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 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
Färdighet 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

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.html

Examination 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.