Engelsk   Dansk
Velkommen til Københavns Universitets kursuskatalog

NDAB05005U  Logik i datalogi: modeller og beviser for systemer (Logik) Årgang 2014/2015

Engelsk titel
Logic in Computer Science: Models and Proofs for Systems (Logik)

Kursusinformation

SprogDansk
Point7,5 ECTS
NiveauBachelor
Varighed1 blok
Placering
Blok 1
Skemagruppe
C (man 13-17 + ons 8-17)
KursuskapacitetIngen begrænsning
Efter- og videreuddannelse
StudienævnStudienævn for Matematik og Datalogi
Udbydende institut
  • Datalogisk Institut
Kursusansvarlig
  • Fritz Henglein (8-6b68716a6f686c7143676c316e7831676e)
Gemt den 04-12-2014
Uddannelse
Bacheloruddannelsen i datalogi
Kursusindhold

Formålet med dette kursus er at lægge et teoretisk grundlag for formel logik, med vægt på logikker, egenskaber, teknikker og algoritmer der er relevante i datalogi. Kurset bygger ovenpå de studerendes eksisterende kendskab til Boolsk logik og matematisk ræsonnement. Det dækker både fundamentale logiske formalismer såvel som mere specialiserede logikker, brugt i modellering, specifikation, og verificering af programmer og hardwaresystemer.

Kurset dækker udsagns- og prædikatlogik i detaljer. Derefter gennemgås mere specialiserede logikker, f.eks. temporallogik, Hoare logik og/eller modallogik, der kan bruges til at ræsonnere om korrektheden af computersystemer.

Målbeskrivelser

Ved kursets afslutning vil den succesfulde studerende have følgende.

 

Viden om:

  • Definitionen af logikker i form af syntaks, semantik, og naturlige deduktionssystemer, og hvordan man formelt ræsonnerer om logiske formler.
  • Et udvalg af bestemte logikker, inklusive udsagnsslogik, prædikatlogik, og temporallogik (f.eks. LTL og CTL).
  • De fundamentale egenskaber for disse logikker, såsom sundhed, fuldstændighed, og (u)afgørlighed.
  • Algoritmer til at transformere logiske formler til normalformer; til at afgøre fundamentale egenskaber for logiske formler såsom tilfredsstillelighed, gyldighed, og (semantisk) følge; og til (symbolsk) modelcheck ved brug af ”binary decision diagrams” (BDD’er).

 

Færdigheder i:

  • At  afgøre og bevise formelle egenskaber for logiske formler (f.eks. tilfredsstillelighed, gyldighed, implikation, og ækvivalens) både ved brug at semantisk argument, og naturlig deduktion.
  • At bevise egenskaber for forholdet mellem semantikken for de viste logikker og deres deduktionssystemer (f.eks. sundhed og fuldstændighed).
  • At anvende specifikke algoritmer til at afgøre egenskaber for logiske formler (f.eks. ”SAT solvers” til tilfredsstillelighed af udsagnslogik; modelcheck af LTL/CTL; brug af BDD’er til at repræsentere Boolske formler og udføre symbolsk modelcheck).
  • At udføre alt ovenstående for varianter af de præsenterede logikker.

 

Kompetence til:

  • At anvende formel logik til at beskrive forskellige virkelighedstro situationer samt udtrykke egenskaber ved programmer (begge af begrænset omfang), og at ræsonnere om disse formelt.
Undervisningsmateriale

Forventes at blive "Logic in Computer Science", 2. udgave; af Michael Huth and Mark Ryan, Cambridge University Press, 2004, ISBN 0-521-54310X.  Supplerende noter.

Undervisningsform
Forelæsninger og øvelses-/​diskussionstimer, obligatoriske afleveringer.

2 undervisningsgange pr. uge, hver gang med ca. 2 forelæsningstimer og 1 øvelses-/​diskussionstime.
Faglige forudsætninger
DiMS eller ækvivalent: familiaritet med basale matematiske formalismer og notation, mængder, grafer, induktionsbeviser, simpel Boolsk logik, ”Store-O” notation, osv.
Tilmelding
Selvbetjeningen på KUnet
Eksamen
Point7,5 ECTS
Prøveform
Skriftlig aflevering, 32 timer
Hjemmeopgave, der skal udformes fuldstændigt indidviduelt. Aflevering i Absalon.
Krav til indstilling til eksamenDer vil blive stillet 6 opgavesæt i løbet af kurset: mindst 5 af de 6 opgavesæt skal afleveres og godkendes for at kunne gå op til eksamen. Der gives mulighed for genaflevering af ikke-beståede opgaver, hvis første aflevering af en opgave er et seriøst løsningsforsøg. Det sidste opgavesæt (nr. 6) kan dog ikke forventes at kunne genafleveres, af tidsmæssige grunde.
HjælpemidlerAlle hjælpemidler tilladt
Bedømmelsesform7-trins skala
CensurformIngen ekstern censur
Flere interne bedømmere
ReeksamenHvis der er 10 eller færre studerende tilmeldt til reeksamen erstattes den skriftlige aflevering med en mundtlig eksamen (30 min. inkl. votering), med forberedelse (60 min.) og skriftlige hjælpemidler.
Kriterier for bedømmelse

Se målbeskrivelsen

Arbejdsbelastning
KategoriTimer
Forelæsninger28
Eksamen17
Teoretiske øvelser14
Forberedelse147
I alt206
Gemt den 04-12-2014