NDAB05005U Logik i datalogi: modeller og beviser for systemer (Logik)

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.