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.
Model-checking og anvendelser. Logikker for specifikation og
ræssonering i multiagent-systemer: logikker for viden, tro,
intentioner, evner og handlinger af individuelle agenter og grupper
af agenter.
Litteraturhenvisninger:
En kombination af forelæsningsnoter og andet materiale vil blive
gjort tilgængelig i løbet af kurset.
