Kursplan för Logik för datavetenskap

Kursplan fastställd 2021-02-26 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 02136
  • Blockschema
  • Sökbar för utbytesstudenterJa

Poängfördelning

0106 Tentamen 7,5 hp
Betygsskala: TH		7,5 hp0 hp0 hp0 hp0 hp0 hp
  • 26 Okt 2023 fm J
  • 03 Jan 2024 em J
  • 28 Aug 2024 fm J

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 given formel är en tautologi
  • förklara begreppet modell för ett första ordningens språk och av temporallogik
  • förklara när en första ordningens och en temporallogiks formel är semantiskt giltigt
  • förklara hur man kontrollerar om en branching-time temporallogik temporär logisk formel är giltig i en given modell
  • förklara betydelsen av sundhet och fullständighet teoremen för sats- och predikatkalky
Färdighet och förmåga:
  • skriva och kontrollera härledningar i naturlig deduktion för sats- och predikatkalkyl
  • 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 verktyg för att lösa problem inom datavetenskap, dvs. hitta buggar med användning av modellkontroll (model checking)

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, Hornklausuler, oavgörbart och uttrycksfullhet av predikatlogik, plus en introduktion till modellkontroll (model checking): 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, se http://www.cs.bham.ac.uk/research/lics/

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 pedagogiskt stöd på grund av funktionsnedsättning.