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)

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.

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.

DiMS eller ækvivalent: familiaritet med basale matematiske formalismer og notation, mængder, grafer, induktionsbeviser, simpel Boolsk logik, ”Store-O” notation, osv.
Forelæsninger og øvelses-/​diskussionstimer, obligatoriske afleveringer.

2 undervisningsgange pr. uge, hver gang med ca. 2 forelæsningstimer og 1 øvelses-/​diskussionstime.
Point
7,5 ECTS
Prøveform
Skriftlig aflevering, 32 timer
Hjemmeopgave, der skal udformes fuldstændigt indidviduelt. Aflevering i Absalon.
Krav til indstilling til eksamen
Der 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ælpemidler
Alle hjælpemidler tilladt
Bedømmelsesform
7-trins skala
Censurform
Ingen ekstern censur
Flere interne bedømmere
Reeksamen
Hvis 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

  • Kategori
  • Timer
  • Forelæsninger
  • 28
  • Eksamen
  • 17
  • Teoretiske øvelser
  • 14
  • Forberedelse
  • 147
  • I alt
  • 206