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 tilgange til programmering ved at definere rekursive prædikater
kommunikere løsninger til problemer på en klar og præcis måde
Kursusindhold:
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).
Bemærkninger:
Formelle Logiske Systemer omfatter dele af forelæsningskursus 02153 Deklarativ Modellering og er samforelæst med kursus 02153.
