Anbefalede faglige forudsætninger for at deltage i modulet

Modulet bygger videre på viden opnået på kurserne: datalogiens teoretiske grundlag, og algoritmer og datastrukturer

Modulets indhold, forløb og pædagogik

FORMÅL 
At den studerende opnår viden og færdigheder om anvendelsen af logikker til at formalisere og løse beregningsmæssige problemer

BEGRUNDELSE 
Logiske sprog og inferensteknikker giver kraftfulde værktøjer til at løse komplekse problemer inden for områder som kunstig intelligens og programanalyse. Kurset vil sætte studerende i stand til at forstå og bruge logikbaseret teknologi

Læringsmål

Viden

Kurset introducerer syntaks, semantik, inferensteknikker og anvendelser af vigtige typer logikker. Specifikke emner dækket i kurset kan omfatte: 

Syntaks, semantik og anvendelser af forsekellige logikker, som f.eks. 

• Udsagnslogik 
• Udvidelser af Udsagnslogik, som f. eks. quantified Boolean formulas og satisfiability modulo theories. 
• Førsteordens prædikatslogik, Højereordens prædikatlogik, Modallogik. 
• Horn clause logik til logiske programmering 
• Hoare logik til programanalyse 

Datastrukturer og teknikker til logisk inferens:  

• Avancerede metoder og datastrukturer til løsning af opfyldelighed (f.eks. DPLL,CDCL,BDDs). 
• Automatiserede bevisteknikker 

Anvendelser: 

• Vidensrepræsentation og ræsonnement i kunstig intelligens 
• Planlægning 
• Analyse af software  

Færdigheder

• forklare centrale teoretiske og praktiske aspekter af logikker introduceret i kurset 
• anvende korrekt fagterminologi og notation 

Kompetencer

• kunne identificere passende logikker til formalisering og løsning af specifikke problemer 
• kunne identificere og anvende egnede algoritmer og softwareværktøjer til løsning af et problem i computational logic 

Undervisningsform

Undervisningen tilrettelægges i henhold til de generelle undervisningsformer for uddannelsen jf. § 17.

Omfang og forventet arbejdsindsats

Det forventes at den studerende bruger 30 timer per ECTS, hvilket for denne aktivitet betyder 150 timer.

Eksamen

Prøver

Prøvens navn	Computational Logic
Prøveform	Skriftlig eller mundtlig
ECTS	5
Tilladte hjælpemidler	Eventuelle tilladte hjælpemidler, vil fremgå af kursussiden i MOODLE
Bedømmelsesform	7-trins-skala
Censur	Intern prøve
Vurderingskriterier	Vurderingskriterierne er angivet i Universitetets eksamensordning

Yderligere informationer

Kontakt: Studienævn for datalogi via cs-sn@cs.aau.dk eller 9940 8854