DM846: Logik til datalogi

Det Naturvidenskabelige Studienævn

Undervisningssprog: På dansk eller engelsk afhængigt af underviser, men engelsk ved internationale studerende
EKA: N340037102, N340037112
Censur: Intern prøve, to eller flere bedømmere, Intern prøve, en bedømmer
Bedømmelse: 7-trinsskala, Bestået/Ikke bestået
Udbudssteder: Odense
Udbudsterminer: Forår
Niveau: Kandidatkursus forhåndsgodkendt som Ph.d.-kursus

STADS ID (UVA): N340037101
ECTS-point: 10

Godkendelsesdato: 02-10-2019


Varighed: 1 semester

Version: Godkendt - aktiv

Kommentar

15016601 (tidligere UVA) er identisk med denne kursusbeskrivelse. 


Indgangskrav

Ingen

Faglige forudsætninger

Den studerende forventes at have opnået en grundlæggende forståelse af matematiske beviser og at være bekendt med det grundlæggende i udsagnslogik og prædikat kalkyle, opnåelige fx ved at have fulgt DM535 Diskrete metoder til datalogi eller MM537 Introduktion til matematiske metoder.

Formål

Formålet med kurset er at give de studerende en baggrund i logik, som fokuserer på forskellige aspekter, der er mest relevante for datalogi.

Målbeskrivelse

Ved kursets afslutning forventes den studerende at have følgende kompetencer:

    • have opnået en forståelse for de teoretiske begreber soundness, completeness og decidability
    • kunne bevise soundness af en bestemt logik
    • vælge logiske rammer bedst egnet til en bestemt datalogisk anvendelse
    • være i stand til at bruge de eksisterende værktøjer til ræsonnement inden for en bestemt logik

    Indhold

    • deduktive systemer til udsagnslogik
    • prædikatslogik og delgrupper heraf, kombinatorisk logik og typeteori
    • Curry-Howard isomorfi
    • modal og temporal logik
    • formel specifikation og validering
    • pi-kalkyle
    • redskaber til logisk ræsonnement

    Litteratur

    Se BlackBoard for pensumlister og yderligere litteraturhenvisninger.

    Eksamensbestemmelser

    Eksamenslement b)

    Tidsmæssig placering

    Juni

    Udprøvninger

    Mundtlig eksamen

    EKA

    N340037102

    Censur

    Intern prøve, to eller flere bedømmere

    Bedømmelse

    7-trinsskala

    Identifikation

    Studiekort

    Sprog

    Følger, som udgangspunkt, undervisningssprog

    Hjælpemidler

    Oplyses på kurset

    ECTS-point

    7

    Uddybende information

    Projekt efterfulgt af mundtlig eksamen.Den studerende udfører et projekt og afleverer en rapport. Evalueringen sker baseret på rapporten og en mundtlig eksamen, hvor projektet præsenteres og underviseren spørger ind til både projektet og til andre emner behandlet i kurset. 

    Eksamensformen ved reeksamen kan være en anden end eksamensformen ved den ordinære eksamen.

    Eksamenslement a)

    Tidsmæssig placering

    Forår

    Udprøvninger

    Opligatoriske opgaver

    EKA

    N340037112

    Censur

    Intern prøve, en bedømmer

    Bedømmelse

    Bestået/Ikke bestået

    Identifikation

    Fulde navn og SDU brugernavn

    Sprog

    Følger, som udgangspunkt, undervisningssprog

    Hjælpemidler

    Oplyses på kurset 

    ECTS-point

    3

    Uddybende information

    Eksamensformen ved reeksamen kan være en anden end eksamensformen ved den ordinære eksamen.

    Vejledende antal undervisningstimer

    62 timer per semester

    Undervisningsform

    På naturvidenskab er undervisningen tilrettelagt efter trefasemodellen dvs. intro, trænings- og studiefasen.

    Introfase: 42 timer

    Træningsfase: 20 timer, heraf:

     - Eksaminatorie: 20 timer

    Ansvarlig underviser

    Navn E-mail Institut
    Luís Cruz-Filipe lcf@imada.sdu.dk

    Yderligere undervisere

    Navn E-mail Institut By
    Marco Peressotti Peressotti@imada.sdu.dk

    Skemaoplysninger

    Administrationsenhed

    Institut for Matematik og Datalogi (datalogi, fiktiv)

    Team hos Registrering & Legalitet

    NAT

    Anbefalede studieforløb

    Profil Program Semester Periode