Stockholms universitet logo, länk till startsida
Go to this page on our english site

Logik i datavetenskap och artificiell intelligens

Kursen behandlar ett urval teman som innehåller betydelsefulla tillämpningar av logik till data- och informationsvetenskaper och artificiell intelligens.

Vi behandlar klassisk första ordningens språk och logik för kunskapsrepresentation och automatisk teorembevisning baserad på första ordningens resolution med unifiering; Logikprogrammering och Prolog; Logiska metoder för programverifiering, till Floyd-Hoare logik för bevis av partiell korrekthet hos datorprogram, samt till metoder för att bevisa att datorprogram terminerar och är fullständigt korrekta; Dynamisk satslogik för program (PDL); Tidslogiker i datavetenskap. Användning av tidslogiker för linjär tid och för förgrenande tid för formell specifikation av egenskaper hos transisitionssystem, och av beräkningar i desamma. Modellprövning och formell verifikation av reaktiva och parallella system.

  • Kursupplägg

    Course webpage

    Undervisning

    Lärare: Valentin Goranko

    Assistent: John Lindqvist

    Undervisningsspråk: engelska

    OBS! Kursen löper över hela terminen på kvartsfart.

    Undervisningen består av föreläsningar och övningar. Närvaro på 70% av undervisningstillfällena är obligatorisk. Kurskrav (obligatorier): inlämning av 3 skriftliga hemuppgifter under kursens gång, inom de tidsbegränsningar som specificeras vid kurstillfällets början, är obligatoriska inslag i kursen. Undervisningen sker på det språk som är angivet för respektive tillfälle för kursen. För mer detaljerad information hänvisas till kursbeskrivningen. Kursbeskrivningen finns tillgänglig senast en månad före kursstart.

    Information om kursens anpassning till gällande rekommendationer för att minska spridning av Corona-viruset

    All undervisning kommer att genomföras online, på Zoom. Tentan kommer att skrivas i ett verktyg för digitala hemtentor.

    Närvarokrav
    Vid kursstart meddelar läraren ifall kravet på minst 70% närvaro på denna kurs (se kursplanen) är i kraft eller ifall det upphävs.

    Examination

    a) Examinationsformer
    Kursen examineras genom 3 skriftliga inlämningsuppgifter och en salstentamen. Principerna för sammanvägning av de enskilda examinationsuppgifterna framgår av betygskriterierna. För mer detaljerad information om examinationen hänvisas till kursbeskrivningen, som finns tillgänglig senast en månad före kursstart.

    b) Betygsskala
    Betygsättningen sker enligt en sjugradig betygsskala:
    A = Utmärkt
    B = Mycket bra
    C = Bra
    D = Tillfredsställande
    E = Tillräckligt
    Fx= Otillräckligt
    F = Helt otillräckligt

    c) Betygskriterier
    De skriftliga betygskriterierna meddelas studenterna vid kursstart. Meddelade målrelaterade betygskriterier är bindande.

    d) Slutbetyg
    För att få slutbetyg på kursen krävs lägst betyget E på samtliga examinationsuppgifter, samt fullgjord närvaro. Om särskilda skäl föreligger kan examinator efter samråd med ansvarig lärare medge den studerande befrielse från skyldigheten att delta i viss obligatorisk undervisning. Studenten kan då åläggas en kompensationsuppgift. Fullgörandet av de skriftliga inlämningsuppgifterna är en förutsättning för att få delta på salskrivningen.

    e) Underkännande
    För varje kurstillfälle erbjuds minst två examinationstillfällen. Det läsår som kurstillfälle saknas erbjuds minst ett examinationstillfälle.
    Studerande som fått betyget Fx eller F på prov två gånger i rad av en och samma examinator har rätt att få en annan examinator utsedd vid nästkommande prov, om inte särskilda skäl talar emot det. Framställan om detta ska göras till institutionsstyrelsen.
    Studerande som fått lägst betyget E får inte genomgå förnyad examination för högre betyg.

    f) Kompletteringsuppgifter
    Möjlighet till komplettering av betyget Fx upp till godkänt betyg på de skriftliga inlämningsuppgifterna kan medges om studenten ligger nära gränsen för godkänt. Uppgiften ska lämnas in inom det tidsintervall som anges av examinator vid kursstart, efter att kompletteringsbehov har meddelats av densamme. Vid godkänd komplettering av enklare formaliafel används betygen A-E. Vid godkänd komplettering av brister av förståelsekaraktär - mindre missförstånd, smärre felaktigheter eller i någon del alltför begränsade resonemang - används betyget E.

  • Schema

    Schema finns tillgängligt senast en månad före kursstart. Vi rekommenderar inte utskrift av scheman då vissa ändringar kan ske. Vid kursstart meddelar utbildningsansvarig institution var du hittar ditt schema under utbildningen.
  • Kurslitteratur

    Observera att kurslitteraturen kan ändras fram till två månader före kursstart.

    Valentin Goranko: Logic as a Tool (Wiley & Sons 2016)
    David Harel, Dexter Kozen & Jerzy Tiuryn: Dynamic Logic (MIT Press 2000)
    Michael Huth & Mark Ryan: Logic in Computer Science (Cambridge University Press, 2nd ed. 2004)
    Stephane Demri, Valentin Goranko & Martin Lange: Temporal Logics in Computer Science (Cambridge University Press 2016)

    Kompletterande litteratur i urval av läraren.

  • Kontakt

    Studievägledare Sama Agahi

    Sama.Agahi@philosophy.su.se

    Studierektor Mattias Högsttröm

    mattias.hogstrom@philosophy.su.se