DM846: Logik til datalogi

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 DM549 Diskrete metoder til datalogi eller MM537 Introduktion til matematiske metoder.

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

I forhold til uddannelsens kompetenceprofil har kurset eksplicit fokus på at:

• give viden om et udvalg af specialiserede modeller og metoder udviklet inden for datalogi baseret på højeste internationale forskning, herunder emner fra fagets forskningsfront
• give viden om datalogiske modeller og metoder beregnet til anvendelser i andre faglige områder
• give færdigheden til at fremsatte hypoteser på kvalificeret teoretisk baggrund og forholde sig kritisk til egne og andres forskningsresultater og videnskabelige modeller
• give kompetence til at planlægge og udføre videnskabelige projekter på højt fagligt niveau herunder styre arbejds- og udviklingssituationer, der er komplekse, uforudsigelige og forudsætter nye løsningsmodeller

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

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

Se itslearning  for pensumlister og yderligere litteraturhenvisninger.

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

• Introfase: 8 timer
• Træningsfase: 8 timer

Aktiviteter i studiefasen:

• læsning af kursusmateriale
• løsning af opgaver relaterede til læsestoffet
• selvstændig opsamling på intro- og træningsfasen

Kontakttimer vil bestå hovedsalig af diskussion af læsestoffet og opgaver.