Kursusmålet er at give de studerende en introduktion til nogle af de grundlæggende deklarative formalismer fra formel datalogi, der kan benyttes til at beskrive, analysere og evaluere aspekter af IT-systemer. Det omfatter såvel teoretiske indsigter som praktiske færdigheder i relevante højniveau-programmeringssprog.
Læringsmål:
En studerende, der fuldt ud har opfyldt kursets mål, vil kunne:
relatere forskellige slags bevissystemer
konstruere formelle beviser i elementære logikker
udnytte udvalgte klassiske og ikke-klassiske logikker
benytte "backtracking" algoritmen til simpel problemløsning
analysere effekten af et deklarativt program
etablere et funktionelt design for et givet problem, således at hovedbegreberne for problemet direkte kan spores i designet
beherske logiske og funktionelle tilgange til programmering ved at definere rekursive prædikater og funktioner
kommunikere løsninger til problemer på en klar og præcis måde
aflede typer for funktionelle programmer
anvende begrebet om funktioner som "first-class citizens"
bevise programkorrekthed baseret på en given metode
formulere programkorrekthed og evaluere forskellige bevisstrategier, og foretage beviser
Kursusindhold:
Den logiske del af kurset dækker logikprogrammering (især Prolog som et "rapid prototyping" værktøj), elementære logikker (herunder propositionelle og første-ordens-logikker), ikke-klassiske logikker (for eksempel temporale logikker), bevissystemer (deduktive systemer og/eller refutationssystemer), og problemløsningsteknikker (såsom "backtracking" algoritmen).
Den funktionelle del af kurset dækker funktionsprogrammering, deklarativ modellering ved brug af et funktionsprogrammeringssprog med et stærkt typebegreb, funktioner som "first-class citizens", programkorrekthed, problemløsningsteknikker, og "rapid prototyping".
