At give den studerende viden og forståelse for en række logiske tilgange, metoder og teknikker benyttet til specifikation, modellering og formel ræssonering i datalogi, kunstig intelligens og multiagent-systemer.
Læringsmål:
En studerende, der fuldt ud har opfyldt kursets mål, vil kunne:
forklare ideerne og principperne bag logisk specifikation og ræssonering i datalogi, AI (kunstig intelligens) og MAS (multiagent-systemer)
benytte klassisk logik til vidensrepræsentation, problem-formalisering, og ræssonering i datalogi og AI
forklare begrebet logisk deduktivt system, og betydningen af sundhed, fuldstændighed, og afgørbarhed af et deduktivt system
forklare og anvende semantiske tableauer og naturlig deduktion i klassisk logik til logisk deduktion og ræssonering
forklare og anvende metoderne fra første-ordens resolution til automatiseret deduktion
forklare de logiske problemer vedrørende model-checking og test af opfyldelighed i konteksten af ræssonering indenfor datalogi og AI
beskrive de forskellige modale og temporale logikker benyttet i datalogi, AI og MAS og forklare de grundlæggende elementer i Kripke-semantikker
vælge og anvende passende modallogiske sprog til vidensrepræsentation, problemanalyse og logisk ræssonering i forskellige områder af datalogi og AI, inkl. temporal og epistemisk ræssonering
beskrive og anvende forskellige logiske systemer til formalisering af, og ræssonering omkring, individuel og fælles viden og strategiske evner i multi-agent systemer
forklare og anvende semantiske tableauer til test af opfyldelighed og logisk deduktion i modale, temporale og epistemiske logikker
individuelt udforske og vurdere den relevante litteratur
Kursusindhold:
Oversigt over klassisk logik som sprog for problemspecifikation og ramme for ræssonering i datalogi og AI ved hjælp af klassiske deduktive systemer: naturlig deduktion, semantiske tableauer og resolution. Automatiseret ræssonering og anvendelser indenfor datalogi og AI. Modale, temporale og epistemiske logikker til specifikation og ræssonering i datalogi og AI. Logikker for specifikation og ræssonering i multiagent-systemer: logikker for viden, tro, intentioner, evner og handlinger af individuelle agenter og grupper af agenter. Semantiske tableauer til test af opfyldelighed og logisk deduktion i modale, temporale og epistemiske logikker.
Litteratur:
En kombination af forelæsningsnoter og andet materiale vil blive gjort tilgængelig i løbet af kurset.
